let Y be non empty set ; 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); 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; ( G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E implies CompF A,G = ((B '/\' C) '/\' D) '/\' E )
assume that
A1:
G = {A,B,C,D,E}
and
A2:
A <> B
and
A3:
A <> C
and
A4:
A <> D
and
A5:
A <> E
; 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 A6:
B = C
;
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 A2, A4, A5, Th7
.=
((B '/\' C) '/\' D) '/\' E
by A6, PARTIT1:15
;
verum end; suppose A7:
B = D
;
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 A2, A3, A5, Th7
.=
((B '/\' D) '/\' C) '/\' E
by A7, PARTIT1:15
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:16
;
verum end; suppose A8:
B = E
;
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 A2, A3, A4, Th7
.=
((B '/\' E) '/\' C) '/\' D
by A8, PARTIT1:15
.=
(B '/\' E) '/\' (C '/\' D)
by PARTIT1:16
.=
(B '/\' (C '/\' D)) '/\' E
by PARTIT1:16
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:16
;
verum end; suppose A9:
C = D
;
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 A2, A3, A5, Th7
.=
(B '/\' (C '/\' D)) '/\' E
by A9, PARTIT1:15
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:16
;
verum end; suppose A10:
C = E
;
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 A2, A3, A4, Th7
.=
(B '/\' (C '/\' E)) '/\' D
by A10, 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
;
verum end; suppose A11:
D = E
;
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 A2, A3, A4, Th7
.=
(B '/\' C) '/\' (D '/\' E)
by A11, 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
;
verum end; suppose A12:
(
B <> C &
B <> D &
B <> E &
C <> D &
C <> E &
D <> E )
;
CompF A,G = ((B '/\' C) '/\' D) '/\' EA13:
( not
D in {A} & not
E in {A} )
by A4, A5, TARSKI:def 1;
A14:
not
B in {A}
by A2, TARSKI:def 1;
G \ {A} = ({A} \/ {B,C,D,E}) \ {A}
by A1, ENUMSET1:47;
then A15:
G \ {A} = ({A} \ {A}) \/ ({B,C,D,E} \ {A})
by XBOOLE_1:42;
A16:
not
C in {A}
by A3, TARSKI:def 1;
A in {A}
by TARSKI:def 1;
then A17:
{A} \ {A} = {}
by ZFMISC_1:68;
{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 A14, 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 A13, ZFMISC_1:72
.=
{B} \/ ({C} \/ {D,E})
by A16, ZFMISC_1:67
.=
{B} \/ {C,D,E}
by ENUMSET1:42
;
then A18:
G \ {A} = ({A} \ {A}) \/ {B,C,D,E}
by A15, ENUMSET1:44;
A19:
((B '/\' C) '/\' D) '/\' E c= '/\' (G \ {A})
proof
let x be
set ;
TARSKI:def 3 ( not x in ((B '/\' C) '/\' D) '/\' E or x in '/\' (G \ {A}) )
assume A20:
x in ((B '/\' C) '/\' D) '/\' E
;
x in '/\' (G \ {A})
then A21:
x <> {}
by EQREL_1:def 6;
x in (INTERSECTION ((B '/\' C) '/\' D),E) \ {{} }
by A20, PARTIT1:def 4;
then consider bcd,
e being
set such that A22:
bcd in (B '/\' C) '/\' D
and A23:
e in E
and A24:
x = bcd /\ e
by SETFAM_1:def 5;
bcd in (INTERSECTION (B '/\' C),D) \ {{} }
by A22, PARTIT1:def 4;
then consider bc,
d being
set such that A25:
bc in B '/\' C
and A26:
d in D
and A27:
bcd = bc /\ d
by SETFAM_1:def 5;
bc in (INTERSECTION B,C) \ {{} }
by A25, PARTIT1:def 4;
then consider b,
c being
set such that A28:
b in B
and A29:
c in C
and A30:
bc = b /\ c
by SETFAM_1:def 5;
set h =
(((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e);
A31:
dom (C .--> c) = {C}
by FUNCOP_1:19;
then A32:
C in dom (C .--> c)
by TARSKI:def 1;
A33:
dom (D .--> d) = {D}
by FUNCOP_1:19;
then A34:
D in dom (D .--> d)
by TARSKI:def 1;
A35:
not
C in dom (D .--> d)
by A12, A33, TARSKI:def 1;
A36:
dom (E .--> e) = {E}
by FUNCOP_1:19;
then
E in dom (E .--> e)
by TARSKI:def 1;
then A37:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E = (E .--> e) . E
by FUNCT_4:14;
then A38:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E = e
by FUNCOP_1:87;
not
C in dom (E .--> e)
by A12, A36, TARSKI:def 1;
then
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C
by FUNCT_4:12;
then
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = ((B .--> b) +* (C .--> c)) . C
by A35, FUNCT_4:12;
then A39:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = (C .--> c) . C
by A32, FUNCT_4:14;
then A40:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = c
by FUNCOP_1:87;
not
D in dom (E .--> e)
by A12, A36, TARSKI:def 1;
then
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D
by FUNCT_4:12;
then A41:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D = (D .--> d) . D
by A34, FUNCT_4:14;
then A42:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D = d
by FUNCOP_1:87;
A43:
not
B in dom (C .--> c)
by A12, A31, TARSKI:def 1;
A44:
not
B in dom (D .--> d)
by A12, A33, TARSKI:def 1;
not
B in dom (E .--> e)
by A12, A36, TARSKI:def 1;
then
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B
by FUNCT_4:12;
then
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = ((B .--> b) +* (C .--> c)) . B
by A44, FUNCT_4:12;
then A45:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = (B .--> b) . B
by A43, FUNCT_4:12;
then A46:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = b
by FUNCOP_1:87;
A47:
for
p being
set st
p in G \ {A} holds
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . p in p
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 A49:
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;
dom (B .--> b) = {B}
by FUNCOP_1:19;
then A50:
dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) =
(({B} \/ {C}) \/ {D}) \/ {E}
by A49, A31, A33, FUNCOP_1:19
.=
({B,C} \/ {D}) \/ {E}
by ENUMSET1:41
.=
{B,C,D} \/ {E}
by ENUMSET1:43
.=
{B,C,D,E}
by ENUMSET1:46
;
then A51:
D in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by ENUMSET1:def 2;
A52:
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)}
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 ;
A56:
C in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A50, ENUMSET1:def 2;
A57:
E in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A50, ENUMSET1:def 2;
A58:
B in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A50, ENUMSET1:def 2;
A59:
{(((((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 A61:
{(((((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 A52, XBOOLE_0:def 10;
reconsider h =
(((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e) as
Function ;
A62:
x c= Intersect F
A69:
rng h <> {}
by A51, FUNCT_1:12;
Intersect F c= x
proof
let t be
set ;
TARSKI:def 3 ( not t in Intersect F or t in x )
assume
t in Intersect F
;
t in x
then A70:
t in meet (rng h)
by A69, SETFAM_1:def 10;
h . D in rng h
by A61, ENUMSET1:def 2;
then A71:
t in h . D
by A70, SETFAM_1:def 1;
h . C in rng h
by A61, ENUMSET1:def 2;
then A72:
t in h . C
by A70, SETFAM_1:def 1;
h . B in rng h
by A61, ENUMSET1:def 2;
then
t in h . B
by A70, SETFAM_1:def 1;
then
t in b /\ c
by A46, A40, A72, XBOOLE_0:def 4;
then A73:
t in (b /\ c) /\ d
by A42, A71, XBOOLE_0:def 4;
h . E in rng h
by A61, ENUMSET1:def 2;
then
t in h . E
by A70, SETFAM_1:def 1;
hence
t in x
by A24, A27, A30, A38, A73, XBOOLE_0:def 4;
verum
end;
then
x = Intersect F
by A62, XBOOLE_0:def 10;
hence
x in '/\' (G \ {A})
by A18, A17, A50, A47, A21, BVFUNC_2:def 1;
verum
end;
'/\' (G \ {A}) c= ((B '/\' C) '/\' D) '/\' E
proof
let x be
set ;
TARSKI:def 3 ( not x in '/\' (G \ {A}) or x in ((B '/\' C) '/\' D) '/\' E )
assume
x in '/\' (G \ {A})
;
x in ((B '/\' C) '/\' D) '/\' E
then consider h being
Function,
F being
Subset-Family of
Y such that A74:
dom h = G \ {A}
and A75:
rng h = F
and A76:
for
d being
set st
d in G \ {A} holds
h . d in d
and A77:
x = Intersect F
and A78:
x <> {}
by BVFUNC_2:def 1;
D in dom h
by A18, A17, A74, ENUMSET1:def 2;
then A79:
h . D in rng h
by FUNCT_1:def 5;
set mbc =
(h . B) /\ (h . C);
A80:
not
x in {{} }
by A78, TARSKI:def 1;
E in G \ {A}
by A18, A17, ENUMSET1:def 2;
then A81:
h . E in E
by A76;
D in G \ {A}
by A18, A17, ENUMSET1:def 2;
then A82:
h . D in D
by A76;
C in G \ {A}
by A18, A17, ENUMSET1:def 2;
then A83:
h . C in C
by A76;
E in dom h
by A18, A17, A74, ENUMSET1:def 2;
then A84:
h . E in rng h
by FUNCT_1:def 5;
set mbcd =
((h . B) /\ (h . C)) /\ (h . D);
B in dom h
by A18, A17, A74, ENUMSET1:def 2;
then A85:
h . B in rng h
by FUNCT_1:def 5;
C in dom h
by A18, A17, A74, ENUMSET1:def 2;
then A86:
h . C in rng h
by FUNCT_1:def 5;
A87:
x c= (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)
proof
let m be
set ;
TARSKI:def 3 ( not m in x or m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) )
assume
m in x
;
m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)
then A88:
m in meet (rng h)
by A75, A77, A85, SETFAM_1:def 10;
then
(
m in h . B &
m in h . C )
by A85, A86, SETFAM_1:def 1;
then A89:
m in (h . B) /\ (h . C)
by XBOOLE_0:def 4;
m in h . D
by A79, A88, SETFAM_1:def 1;
then A90:
m in ((h . B) /\ (h . C)) /\ (h . D)
by A89, XBOOLE_0:def 4;
m in h . E
by A84, A88, SETFAM_1:def 1;
hence
m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)
by A90, XBOOLE_0:def 4;
verum
end;
then
((h . B) /\ (h . C)) /\ (h . D) <> {}
by A78;
then A91:
not
((h . B) /\ (h . C)) /\ (h . D) in {{} }
by TARSKI:def 1;
(h . B) /\ (h . C) <> {}
by A78, A87;
then A92:
not
(h . B) /\ (h . C) in {{} }
by TARSKI:def 1;
B in G \ {A}
by A18, A17, ENUMSET1:def 2;
then
h . B in B
by A76;
then
(h . B) /\ (h . C) in INTERSECTION B,
C
by A83, SETFAM_1:def 5;
then
(h . B) /\ (h . C) in (INTERSECTION B,C) \ {{} }
by A92, 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 A82, SETFAM_1:def 5;
then
((h . B) /\ (h . C)) /\ (h . D) in (INTERSECTION (B '/\' C),D) \ {{} }
by A91, XBOOLE_0:def 5;
then A93:
((h . B) /\ (h . C)) /\ (h . D) in (B '/\' C) '/\' D
by PARTIT1:def 4;
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) c= x
then
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) = x
by A87, XBOOLE_0:def 10;
then
x in INTERSECTION ((B '/\' C) '/\' D),
E
by A81, A93, SETFAM_1:def 5;
then
x in (INTERSECTION ((B '/\' C) '/\' D),E) \ {{} }
by A80, XBOOLE_0:def 5;
hence
x in ((B '/\' C) '/\' D) '/\' E
by PARTIT1:def 4;
verum
end; then
'/\' (G \ {A}) = ((B '/\' C) '/\' D) '/\' E
by A19, XBOOLE_0:def 10;
hence
CompF A,
G = ((B '/\' C) '/\' D) '/\' E
by BVFUNC_2:def 7;
verum end;