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