thus ex G being non empty a_partition of X st
for x being Element of X holds EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } :: thesis: verum
proof
set G = { (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } ;
{ (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } c= bool X
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } or y in bool X )
reconsider yy = y as set by TARSKI:1;
assume y in { (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } ; :: thesis: y in bool X
then consider x being Element of X such that
A4: y = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ;
yy c= X
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in yy or e in X )
consider T being object such that
A5: T in F by XBOOLE_0:def 1;
reconsider T = T as a_partition of X by A5, Def7;
EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } by A5;
then consider f being set such that
A6: f in { (EqClass (x,S)) where S is a_partition of X : S in F } ;
consider S being a_partition of X such that
A7: f = EqClass (x,S) and
S in F by A6;
assume e in yy ; :: thesis: e in X
then e in EqClass (x,S) by A4, A6, A7, SETFAM_1:def 1;
hence e in X ; :: thesis: verum
end;
hence y in bool X ; :: thesis: verum
end;
then reconsider G = { (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } as Subset-Family of X ;
G is a_partition of X
proof
X c= union G
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in union G )
consider T being object such that
A8: T in F by XBOOLE_0:def 1;
assume a in X ; :: thesis: a in union G
then reconsider a1 = a as Element of X ;
reconsider T = T as a_partition of X by A8, Def7;
A9: meet { (EqClass (a1,S)) where S is a_partition of X : S in F } in G ;
A10: for T being set st T in { (EqClass (a1,S)) where S is a_partition of X : S in F } holds
a1 in T
proof
let T be set ; :: thesis: ( T in { (EqClass (a1,S)) where S is a_partition of X : S in F } implies a1 in T )
assume T in { (EqClass (a1,S)) where S is a_partition of X : S in F } ; :: thesis: a1 in T
then ex A being a_partition of X st
( T = EqClass (a1,A) & A in F ) ;
hence a1 in T by Def6; :: thesis: verum
end;
EqClass (a1,T) in { (EqClass (a1,S)) where S is a_partition of X : S in F } by A8;
then a in meet { (EqClass (a1,S)) where S is a_partition of X : S in F } by A10, SETFAM_1:def 1;
hence a in union G by A9, TARSKI:def 4; :: thesis: verum
end;
hence union G = X ; :: according to EQREL_1:def 4 :: thesis: for A being Subset of X st A in G holds
( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) )
let A be Subset of X; :: thesis: ( A in G implies ( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) ) )
consider T being object such that
A11: T in F by XBOOLE_0:def 1;
reconsider T = T as a_partition of X by A11, Def7;
assume A12: A in G ; :: thesis: ( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) )
then consider x being Element of X such that
A13: A = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ;
A14: for Y being set st Y in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
x in Y
proof
let Y be set ; :: thesis: ( Y in { (EqClass (x,S)) where S is a_partition of X : S in F } implies x in Y )
assume Y in { (EqClass (x,S)) where S is a_partition of X : S in F } ; :: thesis: x in Y
then ex T being a_partition of X st
( Y = EqClass (x,T) & T in F ) ;
hence x in Y by Def6; :: thesis: verum
end;
EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } by A11;
hence A <> {} by A13, A14, SETFAM_1:def 1; :: thesis: for B being Subset of X holds
( not B in G or A = B or A misses B )
consider x being Element of X such that
A15: A = meet { (EqClass (x,S)) where S is a_partition of X : S in F } by A12;
let B be Subset of X; :: thesis: ( not B in G or A = B or A misses B )
assume B in G ; :: thesis: ( A = B or A misses B )
then consider y being Element of X such that
A16: B = meet { (EqClass (y,S)) where S is a_partition of X : S in F } ;
thus ( A = B or A misses B ) :: thesis: verum
proof
A17: not { (EqClass (y,S)) where S is a_partition of X : S in F } is empty
proof
consider T being object such that
A18: T in F by XBOOLE_0:def 1;
reconsider T = T as a_partition of X by A18, Def7;
EqClass (y,T) in { (EqClass (y,S)) where S is a_partition of X : S in F } by A18;
hence not { (EqClass (y,S)) where S is a_partition of X : S in F } is empty ; :: thesis: verum
end;
A19: not { (EqClass (x,S)) where S is a_partition of X : S in F } is empty
proof
consider T being object such that
A20: T in F by XBOOLE_0:def 1;
reconsider T = T as a_partition of X by A20, Def7;
EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } by A20;
hence not { (EqClass (x,S)) where S is a_partition of X : S in F } is empty ; :: thesis: verum
end;
now :: thesis: ( not A meets B or A = B or A misses B )
assume A meets B ; :: thesis: ( A = B or A misses B )
then consider c being object such that
A21: ( c in A & c in B ) by XBOOLE_0:3;
c in (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) /\ (meet { (EqClass (y,S)) where S is a_partition of X : S in F } ) by A15, A16, A21, XBOOLE_0:def 4;
then A22: c in meet ( { (EqClass (x,S)) where S is a_partition of X : S in F } \/ { (EqClass (y,S)) where S is a_partition of X : S in F } ) by A19, A17, SETFAM_1:9;
A23: now :: thesis: for T being a_partition of X st T in F holds
c in EqClass (y,T)
let T be a_partition of X; :: thesis: ( T in F implies c in EqClass (y,T) )
assume T in F ; :: thesis: c in EqClass (y,T)
then EqClass (y,T) in { (EqClass (y,S)) where S is a_partition of X : S in F } ;
then EqClass (y,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } \/ { (EqClass (y,S)) where S is a_partition of X : S in F } by XBOOLE_0:def 3;
hence c in EqClass (y,T) by A22, SETFAM_1:def 1; :: thesis: verum
end;
A24: now :: thesis: for T being a_partition of X st T in F holds
c in EqClass (x,T)
let T be a_partition of X; :: thesis: ( T in F implies c in EqClass (x,T) )
assume T in F ; :: thesis: c in EqClass (x,T)
then EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } ;
then EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } \/ { (EqClass (y,S)) where S is a_partition of X : S in F } by XBOOLE_0:def 3;
hence c in EqClass (x,T) by A22, SETFAM_1:def 1; :: thesis: verum
end;
A25: for T being a_partition of X st T in F holds
ex A being object st
( A in EqClass (x,T) & A in EqClass (y,T) )
proof
let T be a_partition of X; :: thesis: ( T in F implies ex A being object st
( A in EqClass (x,T) & A in EqClass (y,T) ) )
assume A26: T in F ; :: thesis: ex A being object st
( A in EqClass (x,T) & A in EqClass (y,T) )
take c ; :: thesis: ( c in EqClass (x,T) & c in EqClass (y,T) )
thus ( c in EqClass (x,T) & c in EqClass (y,T) ) by A24, A23, A26; :: thesis: verum
end;
A27: for T being a_partition of X st T in F holds
EqClass (x,T) meets EqClass (y,T)
proof
let T be a_partition of X; :: thesis: ( T in F implies EqClass (x,T) meets EqClass (y,T) )
assume T in F ; :: thesis: EqClass (x,T) meets EqClass (y,T)
then ex A being object st
( A in EqClass (x,T) & A in EqClass (y,T) ) by A25;
hence EqClass (x,T) meets EqClass (y,T) by XBOOLE_0:3; :: thesis: verum
end;
A28: { (EqClass (y,S)) where S is a_partition of X : S in F } c= { (EqClass (x,S)) where S is a_partition of X : S in F }
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in { (EqClass (y,S)) where S is a_partition of X : S in F } or A in { (EqClass (x,S)) where S is a_partition of X : S in F } )
assume A in { (EqClass (y,S)) where S is a_partition of X : S in F } ; :: thesis: A in { (EqClass (x,S)) where S is a_partition of X : S in F }
then consider T being a_partition of X such that
A29: T in F and
A30: A = EqClass (y,T) by Lm3;
A = EqClass (x,T) by A27, A29, A30, Th41;
hence A in { (EqClass (x,S)) where S is a_partition of X : S in F } by A29; :: thesis: verum
end;
{ (EqClass (x,S)) where S is a_partition of X : S in F } c= { (EqClass (y,S)) where S is a_partition of X : S in F }
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in { (EqClass (x,S)) where S is a_partition of X : S in F } or A in { (EqClass (y,S)) where S is a_partition of X : S in F } )
assume A in { (EqClass (x,S)) where S is a_partition of X : S in F } ; :: thesis: A in { (EqClass (y,S)) where S is a_partition of X : S in F }
then consider T being a_partition of X such that
A31: T in F and
A32: A = EqClass (x,T) by Lm3;
A = EqClass (y,T) by A27, A31, A32, Th41;
hence A in { (EqClass (y,S)) where S is a_partition of X : S in F } by A31; :: thesis: verum
end;
hence ( A = B or A misses B ) by A15, A16, A28, XBOOLE_0:def 10; :: thesis: verum
end;
hence ( A = B or A misses B ) ; :: thesis: verum
end;
end;
then reconsider G = G as non empty a_partition of X ;
take G ; :: thesis: for x being Element of X holds EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }
for x being Element of X holds EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }
proof
let x be Element of X; :: thesis: EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }
A33: now :: thesis: for Y being set st Y in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
x in Y
let Y be set ; :: thesis: ( Y in { (EqClass (x,S)) where S is a_partition of X : S in F } implies x in Y )
assume Y in { (EqClass (x,S)) where S is a_partition of X : S in F } ; :: thesis: x in Y
then ex T being a_partition of X st
( Y = EqClass (x,T) & T in F ) ;
hence x in Y by Def6; :: thesis: verum
end;
not { (EqClass (x,S)) where S is a_partition of X : S in F } is empty
proof
consider T being object such that
A34: T in F by XBOOLE_0:def 1;
reconsider T = T as a_partition of X by A34, Def7;
EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } by A34;
hence not { (EqClass (x,S)) where S is a_partition of X : S in F } is empty ; :: thesis: verum
end;
then ( meet { (EqClass (x,S)) where S is a_partition of X : S in F } in G & x in meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) by A33, SETFAM_1:def 1;
hence EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } by Def6; :: thesis: verum
end;
hence for x being Element of X holds EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ; :: thesis: verum
end;