let I be set ; :: thesis: for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M ex J being MSSetOp of M st
for X being Element of bool M
for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF
let M be ManySortedSet of I; :: thesis: for D being properly-upper-bound MSSubsetFamily of M ex J being MSSetOp of M st
for X being Element of bool M
for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF
let D be properly-upper-bound MSSubsetFamily of M; :: thesis: ex J being MSSetOp of M st
for X being Element of bool M
for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF
set G = bool M;
defpred S₁[ set , set , set ] means for sf being Subset-Family of (M . $3)
for Fi being non empty set st Fi = D . $3 & sf = { z where z is Element of Fi : $2 c= z } holds
$1 = Intersect sf;

A1: now

consider K being ManySortedSet of I such that
A2: K in bool M by PBOOLE:146;
let i be set ; :: thesis: ( i in I implies for x being set st x in (bool M) . i holds
ex y being set st
( y in (bool M) . i & S₁[y,x,i] ) )
assume A3: i in I ; :: thesis: for x being set st x in (bool M) . i holds
ex y being set st
( y in (bool M) . i & S₁[y,x,i] )
reconsider b = (bool M) . i as non empty set by A3;
let x be set ; :: thesis: ( x in (bool M) . i implies ex y being set st
( y in (bool M) . i & S₁[y,x,i] ) )
assume A4: x in (bool M) . i ; :: thesis: ex y being set st
( y in (bool M) . i & S₁[y,x,i] )
dom (K +* (i .--> x)) = I by A3, PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
A5: dom (i .--> x) = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A6: X . i = (i .--> x) . i by A5, FUNCT_4:14
.= x by FUNCOP_1:87 ;
A7: X is Element of bool M

proof

let s be set ; :: according to PBOOLE:def 17 :: thesis: ( not s in I or X . s is Element of (bool M) . s )
assume A8: s in I ; :: thesis: X . s is Element of (bool M) . s

per cases ( s = i or s <> i ) ;

suppose s = i ; :: thesis: X . s is Element of (bool M) . s

hence X . s is Element of (bool M) . s by A4, A6; :: thesis: verum

end;

suppose s <> i ; :: thesis: X . s is Element of (bool M) . s

then not s in dom (i .--> x) by A5, TARSKI:def 1;
then X . s = K . s by FUNCT_4:12;
hence X . s is Element of (bool M) . s by A2, A8, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

then consider SF being V8() MSSubsetFamily of M such that
A9: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) by Th31;
reconsider sf = SF . i as Subset-Family of (M . i) by A3, MSSUBFAM:32;
reconsider q = Intersect sf as Element of b by A3, MBOOLEAN:def 1;
reconsider s = b --> q as Function of b,b ;
take y = s . x; :: thesis: ( y in (bool M) . i & S₁[y,x,i] )
Intersect sf in bool (M . i) ;
then Intersect sf in b by A3, MBOOLEAN:def 1;
hence y in (bool M) . i by A4, FUNCOP_1:13; :: thesis: S₁[y,x,i]
thus S₁[y,x,i] :: thesis: verum

proof

reconsider Di = D . i as non empty set by A3;
A10: SF . i = { z where z is Element of Di : X . i c= z } by A3, A7, A9, Th32;
let sf1 be Subset-Family of (M . i); :: thesis: for Fi being non empty set st Fi = D . i & sf1 = { z where z is Element of Fi : x c= z } holds
y = Intersect sf1
let Fi be non empty set ; :: thesis: ( Fi = D . i & sf1 = { z where z is Element of Fi : x c= z } implies y = Intersect sf1 )
assume ( Fi = D . i & sf1 = { z where z is Element of Fi : x c= z } ) ; :: thesis: y = Intersect sf1
hence y = Intersect sf1 by A4, A6, A10, FUNCOP_1:13; :: thesis: verum

end;

end;

consider J being ManySortedFunction of bool M, bool M such that
A11: for i being set st i in I holds
ex f being Function of ((bool M) . i),((bool M) . i) st
( f = J . i & ( for x being set st x in (bool M) . i holds
S₁[f . x,x,i] ) ) from MSSUBFAM:sch 1(A1);
reconsider J = J as MSSetOp of M ;
take J ; :: thesis: for X being Element of bool M
for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF
let X be Element of bool M; :: thesis: for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF
let SF be V8() MSSubsetFamily of M; :: thesis: ( ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) implies J .. X = meet SF )
assume A12: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ; :: thesis: J .. X = meet SF

now

let i be set ; :: thesis: ( i in I implies (J .. X) . i = (meet SF) . i )
assume A13: i in I ; :: thesis: (J .. X) . i = (meet SF) . i
then consider Q being Subset-Family of (M . i) such that
A14: Q = SF . i and
A15: (meet SF) . i = Intersect Q by MSSUBFAM:def 2;
reconsider Fi = D . i as non empty set by A13;
A16: Q = { z where z is Element of Fi : X . i c= z } by A12, A13, A14, Th32;
X in bool M by MSSUBFAM:12;
then A17: X . i in (bool M) . i by A13, PBOOLE:def 4;
consider f being Function of ((bool M) . i),((bool M) . i) such that
A18: f = J . i and
A19: for x being set st x in (bool M) . i holds
S₁[f . x,x,i] by A11, A13;
dom J = I by PARTFUN1:def 4;
hence (J .. X) . i = f . (X . i) by A13, A18, PRALG_1:def 17
.= (meet SF) . i by A19, A15, A16, A17 ;
:: thesis: verum

end;

hence J .. X = meet SF by PBOOLE:3; :: thesis: verum