let Y be non empty set ; :: thesis: for G being Subset of ()
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 (); :: 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 that
A1: G = {A,B,C} and
A2: A <> B and
A3: C <> A ; :: thesis: CompF (A,G) = B '/\' C
per cases ( B = C or B <> C ) ;
suppose A4: B = C ; :: thesis: CompF (A,G) = B '/\' C
G = {B,C,A} by
.= {B,A} by ;
hence CompF (A,G) = B by
.= B '/\' C by ;
:: thesis: verum
end;
suppose A5: B <> C ; :: thesis: CompF (A,G) = B '/\' C
A6: G \ {A} = ({A} \/ {B,C}) \ {A} by
.= ({A} \ {A}) \/ ({B,C} \ {A}) by XBOOLE_1:42 ;
( not B in {A} & not C in {A} ) by ;
then A7: G \ {A} = ({A} \ {A}) \/ {B,C} by
.= {} \/ {B,C} by XBOOLE_1:37
.= {B,C} ;
A8: '/\' (G \ {A}) c= B '/\' C
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' (G \ {A}) or x in B '/\' C )
reconsider xx = x as set by TARSKI:1;
assume x in '/\' (G \ {A}) ; :: thesis: x in B '/\' C
then consider h being Function, F being Subset-Family of Y such that
A9: dom h = G \ {A} and
A10: rng h = F and
A11: for d being set st d in G \ {A} holds
h . d in d and
A12: x = Intersect F and
A13: x <> {} by BVFUNC_2:def 1;
A14: not x in by ;
B in dom h by ;
then A15: h . B in rng h by FUNCT_1:def 3;
A16: (h . B) /\ (h . C) c= xx
proof
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in (h . B) /\ (h . C) or m in xx )
assume A17: m in (h . B) /\ (h . C) ; :: thesis: m in xx
A18: rng h c= {(h . B),(h . C)}
proof
let u be object ; :: 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 object such that
A19: x1 in dom h and
A20: u = h . x1 by FUNCT_1:def 3;
now :: thesis: ( ( x1 = B & u in {(h . B),(h . C)} ) or ( x1 = C & u in {(h . B),(h . C)} ) )
per cases ( x1 = B or x1 = C ) by ;
case x1 = B ; :: thesis: u in {(h . B),(h . C)}
hence u in {(h . B),(h . C)} by ; :: thesis: verum
end;
case x1 = C ; :: thesis: u in {(h . B),(h . C)}
hence u in {(h . B),(h . C)} by ; :: 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 A21: y in rng h ; :: thesis: m in y
now :: thesis: ( ( y = h . B & m in y ) or ( y = h . C & m in y ) )
per cases ( y = h . B or y = h . C ) by ;
case y = h . B ; :: thesis: m in y
hence m in y by ; :: thesis: verum
end;
case y = h . C ; :: thesis: m in y
hence m in y by ; :: thesis: verum
end;
end;
end;
hence m in y ; :: thesis: verum
end;
then m in meet (rng h) by ;
hence m in xx by ; :: thesis: verum
end;
C in G \ {A} by ;
then A22: h . C in C by A11;
B in G \ {A} by ;
then A23: h . B in B by A11;
C in dom h by ;
then A24: h . C in rng h by FUNCT_1:def 3;
xx c= (h . B) /\ (h . C)
proof
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in xx or m in (h . B) /\ (h . C) )
assume m in xx ; :: thesis: m in (h . B) /\ (h . C)
then m in meet (rng h) by ;
then ( m in h . B & m in h . C ) by ;
hence m in (h . B) /\ (h . C) by XBOOLE_0:def 4; :: thesis: verum
end;
then (h . B) /\ (h . C) = x by ;
then x in INTERSECTION (B,C) by ;
then x in (INTERSECTION (B,C)) \ by ;
hence x in B '/\' C by PARTIT1:def 4; :: thesis: verum
end;
A25: B '/\' C c= '/\' (G \ {A})
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B '/\' C or x in '/\' (G \ {A}) )
reconsider xx = x as set by TARSKI:1;
assume A26: x in B '/\' C ; :: thesis: x in '/\' (G \ {A})
then A27: x <> {} by EQREL_1:def 4;
x in (INTERSECTION (B,C)) \ by ;
then consider a, b being set such that
A28: a in B and
A29: b in C and
A30: x = a /\ b by SETFAM_1:def 5;
set h0 = (B,C) --> (a,b);
A31: dom ((B,C) --> (a,b)) = G \ {A} by ;
A32: rng ((B,C) --> (a,b)) = {a,b} by ;
rng ((B,C) --> (a,b)) c= bool Y
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((B,C) --> (a,b)) or y in bool Y )
assume A33: y in rng ((B,C) --> (a,b)) ; :: thesis: y in bool Y
now :: thesis: ( ( y = a & y in bool Y ) or ( y = b & y in bool Y ) )
per cases ( y = a or y = b ) by ;
end;
end;
hence y in bool Y ; :: thesis: verum
end;
then reconsider F = rng ((B,C) --> (a,b)) as Subset-Family of Y ;
A34: xx c= Intersect F
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in xx or u in Intersect F )
assume A35: u in xx ; :: thesis:
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 A36: y in F ; :: thesis: u in y
now :: thesis: ( ( y = a & u in y ) or ( y = b & u in y ) )
per cases ( y = a or y = b ) by ;
case y = a ; :: thesis: u in y
hence u in y by ; :: thesis: verum
end;
case y = b ; :: thesis: u in y
hence u in y by ; :: thesis: verum
end;
end;
end;
hence u in y ; :: thesis: verum
end;
then u in meet F by ;
hence u in Intersect F by ; :: thesis: verum
end;
A37: 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 A38: d in G \ {A} ; :: thesis: ((B,C) --> (a,b)) . d in d
now :: thesis: ( ( d = B & ((B,C) --> (a,b)) . d in d ) or ( d = C & ((B,C) --> (a,b)) . d in d ) )
per cases ( d = B or d = C ) by ;
case d = B ; :: thesis: ((B,C) --> (a,b)) . d in d
hence ((B,C) --> (a,b)) . d in d by ; :: thesis: verum
end;
case d = C ; :: thesis: ((B,C) --> (a,b)) . d in d
hence ((B,C) --> (a,b)) . d in d by ; :: thesis: verum
end;
end;
end;
hence ((B,C) --> (a,b)) . d in d ; :: thesis: verum
end;
Intersect F c= xx
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Intersect F or u in xx )
assume A39: u in Intersect F ; :: thesis: u in xx
A40: Intersect F = meet F by ;
b in F by ;
then A41: u in b by ;
a in F by ;
then u in a by ;
hence u in xx by ; :: thesis: verum
end;
then x = Intersect F by ;
hence x in '/\' (G \ {A}) by ; :: thesis: verum
end;
CompF (A,G) = '/\' (G \ {A}) by BVFUNC_2:def 7;
hence CompF (A,G) = B '/\' C by ; :: thesis: verum
end;
end;