let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C being a_partition of Y st G = {A,B,C} & A <> B & C <> A holds
CompF A,G = B '/\' C
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C being a_partition of Y st G = {A,B,C} & A <> B & C <> A holds
CompF A,G = B '/\' C
let A, B, C be a_partition of Y; :: thesis: ( G = {A,B,C} & A <> B & C <> A implies CompF A,G = B '/\' C )
assume A1: ( G = {A,B,C} & A <> B & C <> A ) ; :: thesis: CompF A,G = B '/\' C
per cases ( B = C or B <> C ) ;
suppose A2: B = C ; :: thesis: CompF A,G = B '/\' C
G = {B,C,A} by A1, ENUMSET1:100
.= {B,A} by A2, ENUMSET1:70 ;
hence CompF A,G = B by A1, BVFUNC11:7
.= B '/\' C by A2, PARTIT1:15 ;
:: thesis: verum
end;
suppose A3: B <> C ; :: thesis: CompF A,G = B '/\' C
A4: CompF A,G = '/\' (G \ {A}) by BVFUNC_2:def 7;
A5: G \ {A} = ({A} \/ {B,C}) \ {A} by A1, ENUMSET1:42
.= ({A} \ {A}) \/ ({B,C} \ {A}) by XBOOLE_1:42 ;
A6: not B in {A} by A1, TARSKI:def 1;
not C in {A} by A1, TARSKI:def 1;
then A7: G \ {A} = ({A} \ {A}) \/ {B,C} by A5, A6, ZFMISC_1:72
.= {} \/ {B,C} by XBOOLE_1:37
.= {B,C} ;
A8: B '/\' C c= '/\' (G \ {A})
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B '/\' C or x in '/\' (G \ {A}) )
assume A9: x in B '/\' C ; :: thesis: x in '/\' (G \ {A})
then x in (INTERSECTION B,C) \ {{} } by PARTIT1:def 4;
then consider a, b being set such that
A10: ( a in B & b in C & x = a /\ b ) by SETFAM_1:def 5;
set h0 = B,C --> a,b;
A11: dom (B,C --> a,b) = G \ {A} by A7, FUNCT_4:65;
A12: rng (B,C --> a,b) = {a,b} by A3, FUNCT_4:67;
rng (B,C --> a,b) c= bool Y
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (B,C --> a,b) or y in bool Y )
assume A13: y in rng (B,C --> a,b) ; :: thesis: y in bool Y
now
end;
hence y in bool Y ; :: thesis: verum
end;
then reconsider F = rng (B,C --> a,b) as Subset-Family of Y ;
A14: for d being set st d in G \ {A} holds
(B,C --> a,b) . d in d
proof
let d be set ; :: thesis: ( d in G \ {A} implies (B,C --> a,b) . d in d )
assume A15: d in G \ {A} ; :: thesis: (B,C --> a,b) . d in d
now
per cases ( d = B or d = C ) by A7, A15, TARSKI:def 2;
case d = B ; :: thesis: (B,C --> a,b) . d in d
hence (B,C --> a,b) . d in d by A3, A10, FUNCT_4:66; :: thesis: verum
end;
case d = C ; :: thesis: (B,C --> a,b) . d in d
hence (B,C --> a,b) . d in d by A10, FUNCT_4:66; :: thesis: verum
end;
end;
end;
hence (B,C --> a,b) . d in d ; :: thesis: verum
end;
A16: x c= Intersect F
proof
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in x or u in Intersect F )
assume A17: u in x ; :: thesis: u in Intersect F
for y being set st y in F holds
u in y
proof
let y be set ; :: thesis: ( y in F implies u in y )
assume A18: y in F ; :: thesis: u in y
hence u in y ; :: thesis: verum
end;
then u in meet F by A12, SETFAM_1:def 1;
hence u in Intersect F by A12, SETFAM_1:def 10; :: thesis: verum
end;
Intersect F c= x
proof
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in Intersect F or u in x )
assume A19: u in Intersect F ; :: thesis: u in x
A20: ( a in F & b in F ) by A12, TARSKI:def 2;
Intersect F = meet F by A12, SETFAM_1:def 10;
then ( u in a & u in b ) by A19, A20, SETFAM_1:def 1;
hence u in x by A10, XBOOLE_0:def 4; :: thesis: verum
end;
then A21: x = Intersect F by A16, XBOOLE_0:def 10;
x <> {} by A9, EQREL_1:def 6;
hence x in '/\' (G \ {A}) by A11, A14, A21, BVFUNC_2:def 1; :: thesis: verum
end;
'/\' (G \ {A}) c= B '/\' C
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' (G \ {A}) or x in B '/\' C )
assume x in '/\' (G \ {A}) ; :: thesis: x in B '/\' C
then consider h being Function, F being Subset-Family of Y such that
A22: ( dom h = G \ {A} & rng h = F & ( for d being set st d in G \ {A} holds
h . d in d ) & x = Intersect F & x <> {} ) by BVFUNC_2:def 1;
( B in G \ {A} & C in G \ {A} ) by A7, TARSKI:def 2;
then A23: ( h . B in B & h . C in C ) by A22;
( B in dom h & C in dom h ) by A7, A22, TARSKI:def 2;
then A24: ( h . B in rng h & h . C in rng h ) by FUNCT_1:def 5;
A25: not x in {{} } by A22, TARSKI:def 1;
A26: (h . B) /\ (h . C) c= x
proof
let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in (h . B) /\ (h . C) or m in x )
assume A27: m in (h . B) /\ (h . C) ; :: thesis: m in x
A28: rng h c= {(h . B),(h . C)}
proof
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng h or u in {(h . B),(h . C)} )
assume u in rng h ; :: thesis: u in {(h . B),(h . C)}
then consider x1 being set such that
A29: ( x1 in dom h & u = h . x1 ) by FUNCT_1:def 5;
now
per cases ( x1 = B or x1 = C ) by A7, A22, A29, TARSKI:def 2;
case x1 = B ; :: thesis: u in {(h . B),(h . C)}
hence u in {(h . B),(h . C)} by A29, TARSKI:def 2; :: thesis: verum
end;
case x1 = C ; :: thesis: u in {(h . B),(h . C)}
hence u in {(h . B),(h . C)} by A29, TARSKI:def 2; :: thesis: verum
end;
end;
end;
hence u in {(h . B),(h . C)} ; :: thesis: verum
end;
for y being set st y in rng h holds
m in y
proof
let y be set ; :: thesis: ( y in rng h implies m in y )
assume A30: y in rng h ; :: thesis: m in y
now
per cases ( y = h . B or y = h . C ) by A28, A30, TARSKI:def 2;
end;
end;
hence m in y ; :: thesis: verum
end;
then m in meet (rng h) by A24, SETFAM_1:def 1;
hence m in x by A22, A24, SETFAM_1:def 10; :: thesis: verum
end;
x c= (h . B) /\ (h . C)
proof
let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in x or m in (h . B) /\ (h . C) )
assume m in x ; :: thesis: m in (h . B) /\ (h . C)
then m in meet (rng h) by A22, A24, SETFAM_1:def 10;
then ( m in h . B & m in h . C ) by A24, SETFAM_1:def 1;
hence m in (h . B) /\ (h . C) by XBOOLE_0:def 4; :: thesis: verum
end;
then (h . B) /\ (h . C) = x by A26, XBOOLE_0:def 10;
then x in INTERSECTION B,C by A23, SETFAM_1:def 5;
then x in (INTERSECTION B,C) \ {{} } by A25, XBOOLE_0:def 5;
hence x in B '/\' C by PARTIT1:def 4; :: thesis: verum
end;
hence CompF A,G = B '/\' C by A4, A8, XBOOLE_0:def 10; :: thesis: verum
end;
end;