let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E being a_partition of Y st G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E holds
CompF A,G = ((B '/\' C) '/\' D) '/\' E
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D, E being a_partition of Y st G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E holds
CompF A,G = ((B '/\' C) '/\' D) '/\' E
let A, B, C, D, E be a_partition of Y; :: thesis: ( G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E implies CompF A,G = ((B '/\' C) '/\' D) '/\' E )
assume A1:
( G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E )
; :: thesis: CompF A,G = ((B '/\' C) '/\' D) '/\' E
per cases
( B = C or B = D or B = E or C = D or C = E or D = E or ( B <> C & B <> D & B <> E & C <> D & C <> E & D <> E ) )
;
suppose A2:
B = C
;
:: thesis: CompF A,G = ((B '/\' C) '/\' D) '/\' Ethen G =
{A,B,B,D} \/ {E}
by A1, ENUMSET1:50
.=
{B,B,A,D} \/ {E}
by ENUMSET1:110
.=
{B,B,A,D,E}
by ENUMSET1:50
.=
{B,A,D,E}
by ENUMSET1:72
.=
{A,B,D,E}
by ENUMSET1:108
;
hence CompF A,
G =
(B '/\' D) '/\' E
by A1, Th7
.=
((B '/\' C) '/\' D) '/\' E
by A2, PARTIT1:15
;
:: thesis: verum end; suppose A3:
B = D
;
:: thesis: CompF A,G = ((B '/\' C) '/\' D) '/\' Ethen G =
{A,B,C,B} \/ {E}
by A1, ENUMSET1:50
.=
{B,B,A,C} \/ {E}
by ENUMSET1:112
.=
{B,B,A,C,E}
by ENUMSET1:50
.=
{B,A,C,E}
by ENUMSET1:72
.=
{A,B,C,E}
by ENUMSET1:108
;
hence CompF A,
G =
(B '/\' C) '/\' E
by A1, Th7
.=
((B '/\' D) '/\' C) '/\' E
by A3, PARTIT1:15
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:16
;
:: thesis: verum end; suppose A4:
B = E
;
:: thesis: CompF A,G = ((B '/\' C) '/\' D) '/\' Ethen G =
{A} \/ {B,C,D,B}
by A1, ENUMSET1:47
.=
{A} \/ {B,B,C,D}
by ENUMSET1:105
.=
{A} \/ {B,C,D}
by ENUMSET1:71
.=
{A,B,C,D}
by ENUMSET1:44
;
hence CompF A,
G =
(B '/\' C) '/\' D
by A1, Th7
.=
((B '/\' E) '/\' C) '/\' D
by A4, PARTIT1:15
.=
(B '/\' E) '/\' (C '/\' D)
by PARTIT1:16
.=
(B '/\' (C '/\' D)) '/\' E
by PARTIT1:16
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:16
;
:: thesis: verum end; suppose A5:
C = D
;
:: thesis: CompF A,G = ((B '/\' C) '/\' D) '/\' Ethen G =
{A,B,C,C} \/ {E}
by A1, ENUMSET1:50
.=
{C,C,A,B} \/ {E}
by ENUMSET1:118
.=
{C,A,B} \/ {E}
by ENUMSET1:71
.=
{C,A,B,E}
by ENUMSET1:46
.=
{A,B,C,E}
by ENUMSET1:110
;
hence CompF A,
G =
(B '/\' C) '/\' E
by A1, Th7
.=
(B '/\' (C '/\' D)) '/\' E
by A5, PARTIT1:15
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:16
;
:: thesis: verum end; suppose A6:
C = E
;
:: thesis: CompF A,G = ((B '/\' C) '/\' D) '/\' Ethen G =
{A} \/ {B,C,D,C}
by A1, ENUMSET1:47
.=
{A} \/ {C,C,B,D}
by ENUMSET1:117
.=
{A} \/ {C,B,D}
by ENUMSET1:71
.=
{A,C,B,D}
by ENUMSET1:44
.=
{A,B,C,D}
by ENUMSET1:104
;
hence CompF A,
G =
(B '/\' C) '/\' D
by A1, Th7
.=
(B '/\' (C '/\' E)) '/\' D
by A6, PARTIT1:15
.=
B '/\' ((C '/\' E) '/\' D)
by PARTIT1:16
.=
B '/\' ((C '/\' D) '/\' E)
by PARTIT1:16
.=
(B '/\' (C '/\' D)) '/\' E
by PARTIT1:16
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:16
;
:: thesis: verum end; suppose A7:
D = E
;
:: thesis: CompF A,G = ((B '/\' C) '/\' D) '/\' Ethen G =
{A} \/ {B,C,D,D}
by A1, ENUMSET1:47
.=
{A} \/ {D,D,B,C}
by ENUMSET1:118
.=
{A} \/ {D,B,C}
by ENUMSET1:71
.=
{A,D,B,C}
by ENUMSET1:44
.=
{A,B,C,D}
by ENUMSET1:105
;
hence CompF A,
G =
(B '/\' C) '/\' D
by A1, Th7
.=
(B '/\' C) '/\' (D '/\' E)
by A7, PARTIT1:15
.=
B '/\' (C '/\' (D '/\' E))
by PARTIT1:16
.=
B '/\' ((C '/\' D) '/\' E)
by PARTIT1:16
.=
(B '/\' (C '/\' D)) '/\' E
by PARTIT1:16
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:16
;
:: thesis: verum end; suppose A8:
(
B <> C &
B <> D &
B <> E &
C <> D &
C <> E &
D <> E )
;
:: thesis: CompF A,G = ((B '/\' C) '/\' D) '/\' E
G \ {A} = ({A} \/ {B,C,D,E}) \ {A}
by A1, ENUMSET1:47;
then A9:
G \ {A} = ({A} \ {A}) \/ ({B,C,D,E} \ {A})
by XBOOLE_1:42;
A10:
not
B in {A}
by A1, TARSKI:def 1;
A11:
not
C in {A}
by A1, TARSKI:def 1;
A12:
not
D in {A}
by A1, TARSKI:def 1;
A13:
not
E in {A}
by A1, TARSKI:def 1;
{B,C,D,E} \ {A} =
({B} \/ {C,D,E}) \ {A}
by ENUMSET1:44
.=
({B} \ {A}) \/ ({C,D,E} \ {A})
by XBOOLE_1:42
.=
{B} \/ ({C,D,E} \ {A})
by A10, ZFMISC_1:67
.=
{B} \/ (({C} \/ {D,E}) \ {A})
by ENUMSET1:42
.=
{B} \/ (({C} \ {A}) \/ ({D,E} \ {A}))
by XBOOLE_1:42
.=
{B} \/ (({C} \ {A}) \/ {D,E})
by A12, A13, ZFMISC_1:72
.=
{B} \/ ({C} \/ {D,E})
by A11, ZFMISC_1:67
.=
{B} \/ {C,D,E}
by ENUMSET1:42
;
then A14:
G \ {A} = ({A} \ {A}) \/ {B,C,D,E}
by A9, ENUMSET1:44;
A in {A}
by TARSKI:def 1;
then A15:
{A} \ {A} = {}
by ZFMISC_1:68;
A16:
((B '/\' C) '/\' D) '/\' E c= '/\' (G \ {A})
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in ((B '/\' C) '/\' D) '/\' E or x in '/\' (G \ {A}) )
assume A17:
x in ((B '/\' C) '/\' D) '/\' E
;
:: thesis: x in '/\' (G \ {A})
then
x in (INTERSECTION ((B '/\' C) '/\' D),E) \ {{} }
by PARTIT1:def 4;
then consider bcd,
e being
set such that A18:
(
bcd in (B '/\' C) '/\' D &
e in E &
x = bcd /\ e )
by SETFAM_1:def 5;
bcd in (INTERSECTION (B '/\' C),D) \ {{} }
by A18, PARTIT1:def 4;
then consider bc,
d being
set such that A19:
(
bc in B '/\' C &
d in D &
bcd = bc /\ d )
by SETFAM_1:def 5;
bc in (INTERSECTION B,C) \ {{} }
by A19, PARTIT1:def 4;
then consider b,
c being
set such that A20:
(
b in B &
c in C &
bc = b /\ c )
by SETFAM_1:def 5;
set h =
(((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e);
dom ((B .--> b) +* (C .--> c)) = (dom (B .--> b)) \/ (dom (C .--> c))
by FUNCT_4:def 1;
then
dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = ((dom (B .--> b)) \/ (dom (C .--> c))) \/ (dom (D .--> d))
by FUNCT_4:def 1;
then A21:
dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) = (((dom (B .--> b)) \/ (dom (C .--> c))) \/ (dom (D .--> d))) \/ (dom (E .--> e))
by FUNCT_4:def 1;
A22:
dom (B .--> b) = {B}
by FUNCOP_1:19;
A23:
dom (C .--> c) = {C}
by FUNCOP_1:19;
A24:
dom (D .--> d) = {D}
by FUNCOP_1:19;
A25:
dom (E .--> e) = {E}
by FUNCOP_1:19;
A26:
dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) =
(({B} \/ {C}) \/ {D}) \/ {E}
by A21, A22, A23, A24, FUNCOP_1:19
.=
({B,C} \/ {D}) \/ {E}
by ENUMSET1:41
.=
{B,C,D} \/ {E}
by ENUMSET1:43
.=
{B,C,D,E}
by ENUMSET1:46
;
A27:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D = d
A29:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = b
A32:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = c
A35:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E = e
A36:
for
p being
set st
p in G \ {A} holds
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . p in p
A38:
D in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A26, ENUMSET1:def 2;
A39:
B in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A26, ENUMSET1:def 2;
A40:
C in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A26, ENUMSET1:def 2;
A41:
E in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A26, ENUMSET1:def 2;
A42:
rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) c= {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)}
A44:
{(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} c= rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
then A46:
{(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} = rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A42, XBOOLE_0:def 10;
rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) c= bool Y
then reconsider F =
rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) as
Subset-Family of
Y ;
reconsider h =
(((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e) as
Function ;
A48:
rng h <> {}
by A38, FUNCT_1:12;
A49:
x c= Intersect F
Intersect F c= x
proof
let t be
set ;
:: according to TARSKI:def 3 :: thesis: ( not t in Intersect F or t in x )
assume
t in Intersect F
;
:: thesis: t in x
then A56:
t in meet (rng h)
by A48, SETFAM_1:def 10;
(
h . B in rng h &
h . C in rng h &
h . D in rng h &
h . E in rng h )
by A46, ENUMSET1:def 2;
then A57:
(
t in h . B &
t in h . C &
t in h . D &
t in h . E )
by A56, SETFAM_1:def 1;
then
t in b /\ c
by A29, A32, XBOOLE_0:def 4;
then
t in (b /\ c) /\ d
by A27, A57, XBOOLE_0:def 4;
hence
t in x
by A18, A19, A20, A35, A57, XBOOLE_0:def 4;
:: thesis: verum
end;
then A58:
x = Intersect F
by A49, XBOOLE_0:def 10;
x <> {}
by A17, EQREL_1:def 6;
hence
x in '/\' (G \ {A})
by A14, A15, A26, A36, A58, BVFUNC_2:def 1;
:: thesis: verum
end;
'/\' (G \ {A}) c= ((B '/\' C) '/\' D) '/\' E
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in '/\' (G \ {A}) or x in ((B '/\' C) '/\' D) '/\' E )
assume
x in '/\' (G \ {A})
;
:: thesis: x in ((B '/\' C) '/\' D) '/\' E
then consider h being
Function,
F being
Subset-Family of
Y such that A59:
(
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} &
D in G \ {A} &
E in G \ {A} )
by A14, A15, ENUMSET1:def 2;
then A60:
(
h . B in B &
h . C in C &
h . D in D &
h . E in E )
by A59;
(
B in dom h &
C in dom h &
D in dom h &
E in dom h )
by A14, A15, A59, ENUMSET1:def 2;
then A61:
(
h . B in rng h &
h . C in rng h &
h . D in rng h &
h . E in rng h )
by FUNCT_1:def 5;
A62:
not
x in {{} }
by A59, TARSKI:def 1;
A63:
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) c= x
A70:
x c= (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)
then A72:
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) = x
by A63, XBOOLE_0:def 10;
set mbc =
(h . B) /\ (h . C);
set mbcd =
((h . B) /\ (h . C)) /\ (h . D);
((h . B) /\ (h . C)) /\ (h . D) <> {}
by A59, A70;
then A73:
not
((h . B) /\ (h . C)) /\ (h . D) in {{} }
by TARSKI:def 1;
(h . B) /\ (h . C) <> {}
by A59, A70;
then A74:
not
(h . B) /\ (h . C) in {{} }
by TARSKI:def 1;
(h . B) /\ (h . C) in INTERSECTION B,
C
by A60, SETFAM_1:def 5;
then
(h . B) /\ (h . C) in (INTERSECTION B,C) \ {{} }
by A74, XBOOLE_0:def 5;
then
(h . B) /\ (h . C) in B '/\' C
by PARTIT1:def 4;
then
((h . B) /\ (h . C)) /\ (h . D) in INTERSECTION (B '/\' C),
D
by A60, SETFAM_1:def 5;
then
((h . B) /\ (h . C)) /\ (h . D) in (INTERSECTION (B '/\' C),D) \ {{} }
by A73, XBOOLE_0:def 5;
then
((h . B) /\ (h . C)) /\ (h . D) in (B '/\' C) '/\' D
by PARTIT1:def 4;
then
x in INTERSECTION ((B '/\' C) '/\' D),
E
by A60, A72, SETFAM_1:def 5;
then
x in (INTERSECTION ((B '/\' C) '/\' D),E) \ {{} }
by A62, XBOOLE_0:def 5;
hence
x in ((B '/\' C) '/\' D) '/\' E
by PARTIT1:def 4;
:: thesis: verum
end; then
'/\' (G \ {A}) = ((B '/\' C) '/\' D) '/\' E
by A16, XBOOLE_0:def 10;
hence
CompF A,
G = ((B '/\' C) '/\' D) '/\' E
by BVFUNC_2:def 7;
:: thesis: verum end;