let I be set ; 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; 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; 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 S1[ object , object , object ] means ex D2 being set st
( D2 = $2 & ( 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 : D2 c= z } holds
$1 = Intersect sf ) );
A1:
now for i being object st i in I holds
for x being object st x in (bool M) . i holds
ex y being object st
( y in (bool M) . i & S1[y,x,i] )consider K being
ManySortedSet of
I such that A2:
K in bool M
by PBOOLE:134;
let i be
object ;
( i in I implies for x being object st x in (bool M) . i holds
ex y being object st
( y in (bool M) . i & S1[y,x,i] ) )assume A3:
i in I
;
for x being object st x in (bool M) . i holds
ex y being object st
( y in (bool M) . i & S1[y,x,i] )reconsider b =
(bool M) . i as non
empty set by A3;
let x be
object ;
( x in (bool M) . i implies ex y being object st
( y in (bool M) . i & S1[y,x,i] ) )assume A4:
x in (bool M) . i
;
ex y being object st
( y in (bool M) . i & S1[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 2, RELAT_1:def 18;
A5:
dom (i .--> x) = {i}
;
i in {i}
by TARSKI:def 1;
then A6:
X . i =
(i .--> x) . i
by A5, FUNCT_4:13
.=
x
by FUNCOP_1:72
;
A7:
X is
Element of
bool M
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 ;
reconsider y =
s . x as
object ;
take y =
y;
( y in (bool M) . i & S1[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:7;
S1[y,x,i]thus
S1[
y,
x,
i]
verum end;
consider J being ManySortedFunction of bool M, bool M such that
A11:
for i being object st i in I holds
ex f being Function of ((bool M) . i),((bool M) . i) st
( f = J . i & ( for x being object st x in (bool M) . i holds
S1[f . x,x,i] ) )
from MSSUBFAM:sch 1(A1);
reconsider J = J as MSSetOp of M ;
take
J
; 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; 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; ( ( 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 ) )
; J .. X = meet SF
now for i being object st i in I holds
(J .. X) . i = (meet SF) . ilet i be
object ;
( i in I implies (J .. X) . i = (meet SF) . i )assume A13:
i in I
;
(J .. X) . i = (meet SF) . ithen consider Q being
Subset-Family of
(M . i) such that A14:
Q = SF . i
and A15:
(meet SF) . i = Intersect Q
by MSSUBFAM:def 1;
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;
consider f being
Function of
((bool M) . i),
((bool M) . i) such that A18:
f = J . i
and A19:
for
x being
object st
x in (bool M) . i holds
S1[
f . x,
x,
i]
by A11, A13;
A20:
S1[
f . (X . i),
X . i,
i]
by A19, A17;
thus (J .. X) . i =
f . (X . i)
by A13, A18, PRALG_1:def 20
.=
(meet SF) . i
by A15, A16, A20
;
verum end;
hence
J .. X = meet SF
; verum