let Y be non empty set ; for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y st G = {A,B,C,D} & A <> B & A <> C & A <> D holds
CompF (A,G) = (B '/\' C) '/\' D
let G be Subset of (PARTITIONS Y); for A, B, C, D being a_partition of Y st G = {A,B,C,D} & A <> B & A <> C & A <> D holds
CompF (A,G) = (B '/\' C) '/\' D
let A, B, C, D be a_partition of Y; ( G = {A,B,C,D} & A <> B & A <> C & A <> D implies CompF (A,G) = (B '/\' C) '/\' D )
assume that
A1:
G = {A,B,C,D}
and
A2:
A <> B
and
A3:
A <> C
and
A4:
A <> D
; CompF (A,G) = (B '/\' C) '/\' D
per cases
( B = C or B = D or C = D or ( B <> C & B <> D & C <> D ) )
;
suppose A5:
B = C
;
CompF (A,G) = (B '/\' C) '/\' Dthen G =
{B,B,A,D}
by A1, ENUMSET1:71
.=
{B,A,D}
by ENUMSET1:31
.=
{A,B,D}
by ENUMSET1:58
;
hence CompF (
A,
G) =
B '/\' D
by A2, A4, Th4
.=
(B '/\' C) '/\' D
by A5, PARTIT1:13
;
verum end; suppose A6:
B = D
;
CompF (A,G) = (B '/\' C) '/\' Dthen G =
{B,B,A,C}
by A1, ENUMSET1:69
.=
{B,A,C}
by ENUMSET1:31
.=
{A,B,C}
by ENUMSET1:58
;
hence CompF (
A,
G) =
B '/\' C
by A2, A3, Th4
.=
(B '/\' D) '/\' C
by A6, PARTIT1:13
.=
(B '/\' C) '/\' D
by PARTIT1:14
;
verum end; suppose A7:
C = D
;
CompF (A,G) = (B '/\' C) '/\' Dthen G =
{C,C,A,B}
by A1, ENUMSET1:73
.=
{C,A,B}
by ENUMSET1:31
.=
{A,B,C}
by ENUMSET1:59
;
hence CompF (
A,
G) =
B '/\' C
by A2, A3, Th4
.=
B '/\' (C '/\' D)
by A7, PARTIT1:13
.=
(B '/\' C) '/\' D
by PARTIT1:14
;
verum end; suppose A8:
(
B <> C &
B <> D &
C <> D )
;
CompF (A,G) = (B '/\' C) '/\' D
G \ {A} = ({A} \/ {B,C,D}) \ {A}
by A1, ENUMSET1:4;
then A9:
G \ {A} = ({A} \ {A}) \/ ({B,C,D} \ {A})
by XBOOLE_1:42;
A10:
not
B in {A}
by A2, TARSKI:def 1;
A11:
( not
C in {A} & not
D in {A} )
by A3, A4, TARSKI:def 1;
{B,C,D} \ {A} =
({B} \/ {C,D}) \ {A}
by ENUMSET1:2
.=
({B} \ {A}) \/ ({C,D} \ {A})
by XBOOLE_1:42
.=
({B} \ {A}) \/ {C,D}
by A11, ZFMISC_1:63
.=
{B} \/ {C,D}
by A10, ZFMISC_1:59
.=
{B,C,D}
by ENUMSET1:2
;
then A12:
G \ {A} =
{} \/ {B,C,D}
by A9, XBOOLE_1:37
.=
{B,C,D}
;
A13:
(B '/\' C) '/\' D c= '/\' (G \ {A})
proof
let x be
object ;
TARSKI:def 3 ( not x in (B '/\' C) '/\' D or x in '/\' (G \ {A}) )
reconsider xx =
x as
set by TARSKI:1;
assume A14:
x in (B '/\' C) '/\' D
;
x in '/\' (G \ {A})
then A15:
x <> {}
by EQREL_1:def 4;
x in (INTERSECTION ((B '/\' C),D)) \ {{}}
by A14, PARTIT1:def 4;
then consider a,
d being
set such that A16:
a in B '/\' C
and A17:
d in D
and A18:
x = a /\ d
by SETFAM_1:def 5;
a in (INTERSECTION (B,C)) \ {{}}
by A16, PARTIT1:def 4;
then consider b,
c being
set such that A19:
b in B
and A20:
c in C
and A21:
a = b /\ c
by SETFAM_1:def 5;
set h = (
B,
C,
D)
--> (
b,
c,
d);
A22:
((B,C,D) --> (b,c,d)) . D = d
by FUNCT_7:94;
A23:
((B,C,D) --> (b,c,d)) . C = c
by A8, Lm1;
A24:
rng ((B,C,D) --> (b,c,d)) =
{(((B,C,D) --> (b,c,d)) . B),(((B,C,D) --> (b,c,d)) . C),(((B,C,D) --> (b,c,d)) . D)}
by Lm2
.=
{(((B,C,D) --> (b,c,d)) . D),(((B,C,D) --> (b,c,d)) . B),(((B,C,D) --> (b,c,d)) . C)}
by ENUMSET1:59
;
A25:
((B,C,D) --> (b,c,d)) . B = b
by A8, FUNCT_4:134;
rng ((B,C,D) --> (b,c,d)) c= bool Y
proof
let t be
object ;
TARSKI:def 3 ( not t in rng ((B,C,D) --> (b,c,d)) or t in bool Y )
assume A26:
t in rng ((B,C,D) --> (b,c,d))
;
t in bool Y
now ( ( t = ((B,C,D) --> (b,c,d)) . D & t in bool Y ) or ( t = ((B,C,D) --> (b,c,d)) . B & t in bool Y ) or ( t = ((B,C,D) --> (b,c,d)) . C & t in bool Y ) )per cases
( t = ((B,C,D) --> (b,c,d)) . D or t = ((B,C,D) --> (b,c,d)) . B or t = ((B,C,D) --> (b,c,d)) . C )
by A24, A26, ENUMSET1:def 1;
end; end;
hence
t in bool Y
;
verum
end;
then reconsider F =
rng ((B,C,D) --> (b,c,d)) as
Subset-Family of
Y ;
A27:
xx c= Intersect F
proof
let u be
object ;
TARSKI:def 3 ( not u in xx or u in Intersect F )
assume A28:
u in xx
;
u in Intersect F
for
y being
set st
y in F holds
u in y
proof
let y be
set ;
( y in F implies u in y )
assume A29:
y in F
;
u in y
now ( ( y = ((B,C,D) --> (b,c,d)) . D & u in y ) or ( y = ((B,C,D) --> (b,c,d)) . B & u in y ) or ( y = ((B,C,D) --> (b,c,d)) . C & u in y ) )per cases
( y = ((B,C,D) --> (b,c,d)) . D or y = ((B,C,D) --> (b,c,d)) . B or y = ((B,C,D) --> (b,c,d)) . C )
by A24, A29, ENUMSET1:def 1;
end; end;
hence
u in y
;
verum
end;
then
u in meet F
by A24, SETFAM_1:def 1;
hence
u in Intersect F
by A24, SETFAM_1:def 9;
verum
end;
A32:
for
p being
set st
p in G \ {A} holds
((B,C,D) --> (b,c,d)) . p in p
proof
let p be
set ;
( p in G \ {A} implies ((B,C,D) --> (b,c,d)) . p in p )
assume A33:
p in G \ {A}
;
((B,C,D) --> (b,c,d)) . p in p
now ( ( p = D & ((B,C,D) --> (b,c,d)) . p in p ) or ( p = B & ((B,C,D) --> (b,c,d)) . p in p ) or ( p = C & ((B,C,D) --> (b,c,d)) . p in p ) )end;
hence
((B,C,D) --> (b,c,d)) . p in p
;
verum
end;
A34:
dom ((B,C,D) --> (b,c,d)) = {B,C,D}
by FUNCT_4:128;
then
D in dom ((B,C,D) --> (b,c,d))
by ENUMSET1:def 1;
then A35:
rng ((B,C,D) --> (b,c,d)) <> {}
by FUNCT_1:3;
Intersect F c= xx
proof
let t be
object ;
TARSKI:def 3 ( not t in Intersect F or t in xx )
assume
t in Intersect F
;
t in xx
then A36:
t in meet (rng ((B,C,D) --> (b,c,d)))
by A35, SETFAM_1:def 9;
((B,C,D) --> (b,c,d)) . D in rng ((B,C,D) --> (b,c,d))
by A24, ENUMSET1:def 1;
then A37:
t in ((B,C,D) --> (b,c,d)) . D
by A36, SETFAM_1:def 1;
((B,C,D) --> (b,c,d)) . C in rng ((B,C,D) --> (b,c,d))
by A24, ENUMSET1:def 1;
then A38:
t in ((B,C,D) --> (b,c,d)) . C
by A36, SETFAM_1:def 1;
((B,C,D) --> (b,c,d)) . B in rng ((B,C,D) --> (b,c,d))
by A24, ENUMSET1:def 1;
then
t in ((B,C,D) --> (b,c,d)) . B
by A36, SETFAM_1:def 1;
then
t in b /\ c
by A25, A23, A38, XBOOLE_0:def 4;
hence
t in xx
by A18, A21, A22, A37, XBOOLE_0:def 4;
verum
end;
then
x = Intersect F
by A27, XBOOLE_0:def 10;
hence
x in '/\' (G \ {A})
by A12, A34, A32, A15, BVFUNC_2:def 1;
verum
end;
'/\' (G \ {A}) c= (B '/\' C) '/\' D
proof
let x be
object ;
TARSKI:def 3 ( not x in '/\' (G \ {A}) or x in (B '/\' C) '/\' D )
reconsider xx =
x as
set by TARSKI:1;
assume
x in '/\' (G \ {A})
;
x in (B '/\' C) '/\' D
then consider h being
Function,
F being
Subset-Family of
Y such that A39:
dom h = G \ {A}
and A40:
rng h = F
and A41:
for
d being
set st
d in G \ {A} holds
h . d in d
and A42:
x = Intersect F
and A43:
x <> {}
by BVFUNC_2:def 1;
D in dom h
by A12, A39, ENUMSET1:def 1;
then A44:
h . D in rng h
by FUNCT_1:def 3;
set m =
(h . B) /\ (h . C);
B in dom h
by A12, A39, ENUMSET1:def 1;
then A45:
h . B in rng h
by FUNCT_1:def 3;
C in dom h
by A12, A39, ENUMSET1:def 1;
then A46:
h . C in rng h
by FUNCT_1:def 3;
A47:
xx c= ((h . B) /\ (h . C)) /\ (h . D)
then
(h . B) /\ (h . C) <> {}
by A43;
then A50:
not
(h . B) /\ (h . C) in {{}}
by TARSKI:def 1;
D in G \ {A}
by A12, ENUMSET1:def 1;
then A51:
h . D in D
by A41;
A52:
not
x in {{}}
by A43, TARSKI:def 1;
C in G \ {A}
by A12, ENUMSET1:def 1;
then A53:
h . C in C
by A41;
B in G \ {A}
by A12, ENUMSET1:def 1;
then
h . B in B
by A41;
then
(h . B) /\ (h . C) in INTERSECTION (
B,
C)
by A53, SETFAM_1:def 5;
then
(h . B) /\ (h . C) in (INTERSECTION (B,C)) \ {{}}
by A50, XBOOLE_0:def 5;
then A54:
(h . B) /\ (h . C) in B '/\' C
by PARTIT1:def 4;
((h . B) /\ (h . C)) /\ (h . D) c= xx
proof
let m be
object ;
TARSKI:def 3 ( not m in ((h . B) /\ (h . C)) /\ (h . D) or m in xx )
assume A55:
m in ((h . B) /\ (h . C)) /\ (h . D)
;
m in xx
then A56:
m in (h . B) /\ (h . C)
by XBOOLE_0:def 4;
A57:
rng h c= {(h . B),(h . C),(h . D)}
proof
let u be
object ;
TARSKI:def 3 ( not u in rng h or u in {(h . B),(h . C),(h . D)} )
assume
u in rng h
;
u in {(h . B),(h . C),(h . D)}
then consider x1 being
object such that A58:
x1 in dom h
and A59:
u = h . x1
by FUNCT_1:def 3;
now ( ( x1 = B & u in {(h . B),(h . C),(h . D)} ) or ( x1 = C & u in {(h . B),(h . C),(h . D)} ) or ( x1 = D & u in {(h . B),(h . C),(h . D)} ) )end;
hence
u in {(h . B),(h . C),(h . D)}
;
verum
end;
for
y being
set st
y in rng h holds
m in y
proof
let y be
set ;
( y in rng h implies m in y )
assume A60:
y in rng h
;
m in y
now ( ( y = h . B & m in y ) or ( y = h . C & m in y ) or ( y = h . D & m in y ) )end;
hence
m in y
;
verum
end;
then
m in meet (rng h)
by A45, SETFAM_1:def 1;
hence
m in xx
by A40, A42, A45, SETFAM_1:def 9;
verum
end;
then
((h . B) /\ (h . C)) /\ (h . D) = x
by A47, XBOOLE_0:def 10;
then
x in INTERSECTION (
(B '/\' C),
D)
by A51, A54, SETFAM_1:def 5;
then
x in (INTERSECTION ((B '/\' C),D)) \ {{}}
by A52, XBOOLE_0:def 5;
hence
x in (B '/\' C) '/\' D
by PARTIT1:def 4;
verum
end; then
'/\' (G \ {A}) = (B '/\' C) '/\' D
by A13, XBOOLE_0:def 10;
hence
CompF (
A,
G)
= (B '/\' C) '/\' D
by BVFUNC_2:def 7;
verum end; end;