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 that

A1: G = {A,B,C} and

A2: A <> B and

A3: C <> A ; :: thesis: CompF (A,G) = B '/\' C

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 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 )
;

end;

suppose A4:
B = C
; :: thesis: CompF (A,G) = B '/\' C

G =
{B,C,A}
by A1, ENUMSET1:59

.= {B,A} by A4, ENUMSET1:30 ;

hence CompF (A,G) = B by A2, BVFUNC11:7

.= B '/\' C by A4, PARTIT1:13 ;

:: thesis: verum

end;.= {B,A} by A4, ENUMSET1:30 ;

hence CompF (A,G) = B by A2, BVFUNC11:7

.= B '/\' C by A4, PARTIT1:13 ;

:: thesis: verum

suppose A5:
B <> C
; :: thesis: CompF (A,G) = B '/\' C

A6: G \ {A} =
({A} \/ {B,C}) \ {A}
by A1, ENUMSET1:2

.= ({A} \ {A}) \/ ({B,C} \ {A}) by XBOOLE_1:42 ;

( not B in {A} & not C in {A} ) by A2, A3, TARSKI:def 1;

then A7: G \ {A} = ({A} \ {A}) \/ {B,C} by A6, ZFMISC_1:63

.= {} \/ {B,C} by XBOOLE_1:37

.= {B,C} ;

A8: '/\' (G \ {A}) c= B '/\' C

hence CompF (A,G) = B '/\' C by A25, A8, XBOOLE_0:def 10; :: thesis: verum

end;.= ({A} \ {A}) \/ ({B,C} \ {A}) by XBOOLE_1:42 ;

( not B in {A} & not C in {A} ) by A2, A3, TARSKI:def 1;

then A7: G \ {A} = ({A} \ {A}) \/ {B,C} by A6, ZFMISC_1:63

.= {} \/ {B,C} by XBOOLE_1:37

.= {B,C} ;

A8: '/\' (G \ {A}) c= B '/\' C

proof

A25:
B '/\' C c= '/\' (G \ {A})
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 A13, TARSKI:def 1;

B in dom h by A7, A9, TARSKI:def 2;

then A15: h . B in rng h by FUNCT_1:def 3;

A16: (h . B) /\ (h . C) c= xx

then A22: h . C in C by A11;

B in G \ {A} by A7, TARSKI:def 2;

then A23: h . B in B by A11;

C in dom h by A7, A9, TARSKI:def 2;

then A24: h . C in rng h by FUNCT_1:def 3;

xx c= (h . B) /\ (h . C)

then x in INTERSECTION (B,C) by A23, A22, SETFAM_1:def 5;

then x in (INTERSECTION (B,C)) \ {{}} by A14, XBOOLE_0:def 5;

hence x in B '/\' C by PARTIT1:def 4; :: thesis: verum

end;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 A13, TARSKI:def 1;

B in dom h by A7, A9, TARSKI:def 2;

then A15: h . B in rng h by FUNCT_1:def 3;

A16: (h . B) /\ (h . C) c= xx

proof

C in G \ {A}
by A7, TARSKI:def 2;
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)}

m in y

hence m in xx by A10, A12, A15, SETFAM_1:def 9; :: thesis: verum

end;assume A17: m in (h . B) /\ (h . C) ; :: thesis: m in xx

A18: rng h c= {(h . B),(h . C)}

proof

for y being set st y in rng h holds
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;

end;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)} ) )

hence
u in {(h . B),(h . C)}
; :: thesis: verumend;

m in y

proof

then
m in meet (rng h)
by A15, SETFAM_1:def 1;
let y be set ; :: thesis: ( y in rng h implies m in y )

assume A21: y in rng h ; :: thesis: m in y

end;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 ) )end;

hence
m in y
; :: thesis: verumhence m in xx by A10, A12, A15, SETFAM_1:def 9; :: thesis: verum

then A22: h . C in C by A11;

B in G \ {A} by A7, TARSKI:def 2;

then A23: h . B in B by A11;

C in dom h by A7, A9, TARSKI:def 2;

then A24: h . C in rng h by FUNCT_1:def 3;

xx c= (h . B) /\ (h . C)

proof

then
(h . B) /\ (h . C) = x
by A16, XBOOLE_0:def 10;
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 A10, A12, A15, SETFAM_1:def 9;

then ( m in h . B & m in h . C ) by A15, A24, SETFAM_1:def 1;

hence m in (h . B) /\ (h . C) by XBOOLE_0:def 4; :: thesis: verum

end;assume m in xx ; :: thesis: m in (h . B) /\ (h . C)

then m in meet (rng h) by A10, A12, A15, SETFAM_1:def 9;

then ( m in h . B & m in h . C ) by A15, A24, SETFAM_1:def 1;

hence m in (h . B) /\ (h . C) by XBOOLE_0:def 4; :: thesis: verum

then x in INTERSECTION (B,C) by A23, A22, SETFAM_1:def 5;

then x in (INTERSECTION (B,C)) \ {{}} by A14, XBOOLE_0:def 5;

hence x in B '/\' C by PARTIT1:def 4; :: thesis: verum

proof

CompF (A,G) = '/\' (G \ {A})
by BVFUNC_2:def 7;
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 A26, PARTIT1:def 4;

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 A7, FUNCT_4:62;

A32: rng ((B,C) --> (a,b)) = {a,b} by A5, FUNCT_4:64;

rng ((B,C) --> (a,b)) c= bool Y

A34: xx c= Intersect F

((B,C) --> (a,b)) . d in d

hence x in '/\' (G \ {A}) by A31, A37, A27, BVFUNC_2:def 1; :: thesis: verum

end;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 A26, PARTIT1:def 4;

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 A7, FUNCT_4:62;

A32: rng ((B,C) --> (a,b)) = {a,b} by A5, FUNCT_4:64;

rng ((B,C) --> (a,b)) c= bool Y

proof

then reconsider F = rng ((B,C) --> (a,b)) as Subset-Family of Y ;
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

hence y in bool Y ; :: thesis: verum

end;assume A33: y in rng ((B,C) --> (a,b)) ; :: thesis: y in bool Y

hence y in bool Y ; :: thesis: verum

A34: xx c= Intersect F

proof

A37:
for d being set st d in G \ {A} holds
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: u in Intersect F

for y being set st y in F holds

u in y

hence u in Intersect F by A32, SETFAM_1:def 9; :: thesis: verum

end;assume A35: u in xx ; :: thesis: u in Intersect F

for y being set st y in F holds

u in y

proof

then
u in meet F
by A32, SETFAM_1:def 1;
let y be set ; :: thesis: ( y in F implies u in y )

assume A36: y in F ; :: thesis: u in y

end;assume A36: y in F ; :: thesis: u in y

now :: thesis: ( ( y = a & u in y ) or ( y = b & u in y ) )end;

hence
u in y
; :: thesis: verumhence u in Intersect F by A32, SETFAM_1:def 9; :: thesis: verum

((B,C) --> (a,b)) . d in d

proof

Intersect F c= xx
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

end;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 ) )

hence
((B,C) --> (a,b)) . d in d
; :: thesis: verumend;

proof

then
x = Intersect F
by A34, XBOOLE_0:def 10;
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 A32, SETFAM_1:def 9;

b in F by A32, TARSKI:def 2;

then A41: u in b by A39, A40, SETFAM_1:def 1;

a in F by A32, TARSKI:def 2;

then u in a by A39, A40, SETFAM_1:def 1;

hence u in xx by A30, A41, XBOOLE_0:def 4; :: thesis: verum

end;assume A39: u in Intersect F ; :: thesis: u in xx

A40: Intersect F = meet F by A32, SETFAM_1:def 9;

b in F by A32, TARSKI:def 2;

then A41: u in b by A39, A40, SETFAM_1:def 1;

a in F by A32, TARSKI:def 2;

then u in a by A39, A40, SETFAM_1:def 1;

hence u in xx by A30, A41, XBOOLE_0:def 4; :: thesis: verum

hence x in '/\' (G \ {A}) by A31, A37, A27, BVFUNC_2:def 1; :: thesis: verum

hence CompF (A,G) = B '/\' C by A25, A8, XBOOLE_0:def 10; :: thesis: verum