defpred S_{1}[ set ] means ex h being Function ex F being Subset-Family of Y st

( dom h = G & rng h = F & ( for d being set st d in G holds

h . d in d ) & $1 = Intersect F & $1 <> {} );

consider X being set such that

A1: for x being set holds

( x in X iff ( x in bool Y & S_{1}[x] ) )
from XFAMILY:sch 1();

A2: for A being Subset of Y st A in X holds

( A <> {} & ( for B being Subset of Y holds

( not B in X or A = B or A misses B ) ) )

( x in X iff ex h being Function ex F being Subset-Family of Y st

( dom h = G & rng h = F & ( for d being set st d in G holds

h . d in d ) & x = Intersect F & x <> {} ) ) ) )

X c= bool Y by A1;

then reconsider X = X as Subset-Family of Y ;

X is a_partition of Y by A24, A2, A21, EQREL_1:def 4, XBOOLE_0:def 10;

hence ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds

( x in X iff ex h being Function ex F being Subset-Family of Y st

( dom h = G & rng h = F & ( for d being set st d in G holds

h . d in d ) & x = Intersect F & x <> {} ) ) ) ) by A1; :: thesis: verum

( dom h = G & rng h = F & ( for d being set st d in G holds

h . d in d ) & $1 = Intersect F & $1 <> {} );

consider X being set such that

A1: for x being set holds

( x in X iff ( x in bool Y & S

A2: for A being Subset of Y st A in X holds

( A <> {} & ( for B being Subset of Y holds

( not B in X or A = B or A misses B ) ) )

proof

A21:
Y c= union X
let A be Subset of Y; :: thesis: ( A in X implies ( A <> {} & ( for B being Subset of Y holds

( not B in X or A = B or A misses B ) ) ) )

assume A in X ; :: thesis: ( A <> {} & ( for B being Subset of Y holds

( not B in X or A = B or A misses B ) ) )

then consider h1 being Function, F1 being Subset-Family of Y such that

A3: dom h1 = G and

A4: rng h1 = F1 and

A5: for d being set st d in G holds

h1 . d in d and

A6: A = Intersect F1 and

A7: A <> {} by A1;

thus A <> {} by A7; :: thesis: for B being Subset of Y holds

( not B in X or A = B or A misses B )

let B be Subset of Y; :: thesis: ( not B in X or A = B or A misses B )

assume B in X ; :: thesis: ( A = B or A misses B )

then consider h2 being Function, F2 being Subset-Family of Y such that

A8: dom h2 = G and

A9: rng h2 = F2 and

A10: for d being set st d in G holds

h2 . d in d and

A11: B = Intersect F2 and

B <> {} by A1;

end;( not B in X or A = B or A misses B ) ) ) )

assume A in X ; :: thesis: ( A <> {} & ( for B being Subset of Y holds

( not B in X or A = B or A misses B ) ) )

then consider h1 being Function, F1 being Subset-Family of Y such that

A3: dom h1 = G and

A4: rng h1 = F1 and

A5: for d being set st d in G holds

h1 . d in d and

A6: A = Intersect F1 and

A7: A <> {} by A1;

thus A <> {} by A7; :: thesis: for B being Subset of Y holds

( not B in X or A = B or A misses B )

let B be Subset of Y; :: thesis: ( not B in X or A = B or A misses B )

assume B in X ; :: thesis: ( A = B or A misses B )

then consider h2 being Function, F2 being Subset-Family of Y such that

A8: dom h2 = G and

A9: rng h2 = F2 and

A10: for d being set st d in G holds

h2 . d in d and

A11: B = Intersect F2 and

B <> {} by A1;

per cases
( G = {} or G <> {} )
;

end;

suppose A12:
G = {}
; :: thesis: ( A = B or A misses B )

then
rng h1 = {}
by A3, RELAT_1:42;

hence ( A = B or A misses B ) by A4, A6, A8, A9, A11, A12, RELAT_1:42; :: thesis: verum

end;hence ( A = B or A misses B ) by A4, A6, A8, A9, A11, A12, RELAT_1:42; :: thesis: verum

suppose A13:
G <> {}
; :: thesis: ( A = B or A misses B )

end;

now :: thesis: ( not A meets B or A = B or A misses B )

hence
( A = B or A misses B )
; :: thesis: verumassume
A meets B
; :: thesis: ( A = B or A misses B )

then consider p being object such that

A14: p in A and

A15: p in B by XBOOLE_0:3;

A16: p in meet (rng h2) by A9, A11, A13, A15, A8, RELAT_1:42, SETFAM_1:def 9;

A17: p in meet (rng h1) by A4, A6, A3, A13, A14, RELAT_1:42, SETFAM_1:def 9;

for g being object st g in G holds

h1 . g = h2 . g

end;then consider p being object such that

A14: p in A and

A15: p in B by XBOOLE_0:3;

A16: p in meet (rng h2) by A9, A11, A13, A15, A8, RELAT_1:42, SETFAM_1:def 9;

A17: p in meet (rng h1) by A4, A6, A3, A13, A14, RELAT_1:42, SETFAM_1:def 9;

for g being object st g in G holds

h1 . g = h2 . g

proof

hence
( A = B or A misses B )
by A3, A4, A6, A8, A9, A11, FUNCT_1:2; :: thesis: verum
let g be object ; :: thesis: ( g in G implies h1 . g = h2 . g )

assume A18: g in G ; :: thesis: h1 . g = h2 . g

then reconsider g = g as a_partition of Y by PARTIT1:def 3;

h1 . g in rng h1 by A3, A18, FUNCT_1:def 3;

then A19: p in h1 . g by A17, SETFAM_1:def 1;

h2 . g in rng h2 by A8, A18, FUNCT_1:def 3;

then A20: p in h2 . g by A16, SETFAM_1:def 1;

( h1 . g in g & h2 . g in g ) by A5, A10, A18;

hence h1 . g = h2 . g by A19, A20, EQREL_1:def 4, XBOOLE_0:3; :: thesis: verum

end;assume A18: g in G ; :: thesis: h1 . g = h2 . g

then reconsider g = g as a_partition of Y by PARTIT1:def 3;

h1 . g in rng h1 by A3, A18, FUNCT_1:def 3;

then A19: p in h1 . g by A17, SETFAM_1:def 1;

h2 . g in rng h2 by A8, A18, FUNCT_1:def 3;

then A20: p in h2 . g by A16, SETFAM_1:def 1;

( h1 . g in g & h2 . g in g ) by A5, A10, A18;

hence h1 . g = h2 . g by A19, A20, EQREL_1:def 4, XBOOLE_0:3; :: thesis: verum

proof

A24:
union X c= Y
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in union X )

assume y in Y ; :: thesis: y in union X

then reconsider y = y as Element of Y ;

consider a being Subset of Y such that

A22: y in a and

A23: ex h being Function ex F being Subset-Family of Y st

( dom h = G & rng h = F & ( for d being set st d in G holds

h . d in d ) & a = Intersect F & a <> {} ) by Th1;

a in X by A1, A23;

hence y in union X by A22, TARSKI:def 4; :: thesis: verum

end;assume y in Y ; :: thesis: y in union X

then reconsider y = y as Element of Y ;

consider a being Subset of Y such that

A22: y in a and

A23: ex h being Function ex F being Subset-Family of Y st

( dom h = G & rng h = F & ( for d being set st d in G holds

h . d in d ) & a = Intersect F & a <> {} ) by Th1;

a in X by A1, A23;

hence y in union X by A22, TARSKI:def 4; :: thesis: verum

proof

take
X
; :: thesis: ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union X or a in Y )

assume a in union X ; :: thesis: a in Y

then consider p being set such that

A25: a in p and

A26: p in X by TARSKI:def 4;

ex h being Function ex F being Subset-Family of Y st

( dom h = G & rng h = F & ( for d being set st d in G holds

h . d in d ) & p = Intersect F & p <> {} ) by A1, A26;

hence a in Y by A25; :: thesis: verum

end;assume a in union X ; :: thesis: a in Y

then consider p being set such that

A25: a in p and

A26: p in X by TARSKI:def 4;

ex h being Function ex F being Subset-Family of Y st

( dom h = G & rng h = F & ( for d being set st d in G holds

h . d in d ) & p = Intersect F & p <> {} ) by A1, A26;

hence a in Y by A25; :: thesis: verum

( x in X iff ex h being Function ex F being Subset-Family of Y st

( dom h = G & rng h = F & ( for d being set st d in G holds

h . d in d ) & x = Intersect F & x <> {} ) ) ) )

X c= bool Y by A1;

then reconsider X = X as Subset-Family of Y ;

X is a_partition of Y by A24, A2, A21, EQREL_1:def 4, XBOOLE_0:def 10;

hence ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds

( x in X iff ex h being Function ex F being Subset-Family of Y st

( dom h = G & rng h = F & ( for d being set st d in G holds

h . d in d ) & x = Intersect F & x <> {} ) ) ) ) by A1; :: thesis: verum