let Y be non empty set ; :: thesis: for G being Subset of ()
for A, B being a_partition of Y st G = {A,B} & A <> B holds
'/\' G = A '/\' B

let G be Subset of (); :: thesis: for A, B being a_partition of Y st G = {A,B} & A <> B holds
'/\' G = A '/\' B

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