let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF A,G = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF A,G = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
let A, B, C, D, E, F, J be a_partition of Y; :: thesis: ( G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J implies CompF A,G = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J )
assume A1:
( G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J )
; :: thesis: CompF A,G = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
A2:
CompF A,G = '/\' (G \ {A})
by BVFUNC_2:def 7;
A3:
G \ {A} = ({A} \/ {B,C,D,E,F,J}) \ {A}
by A1, ENUMSET1:56;
A4:
not B in {A}
by A1, TARSKI:def 1;
A5:
not C in {A}
by A1, TARSKI:def 1;
A6:
not D in {A}
by A1, TARSKI:def 1;
A7:
not E in {A}
by A1, TARSKI:def 1;
A8:
not F in {A}
by A1, TARSKI:def 1;
A9:
not J in {A}
by A1, TARSKI:def 1;
A10:
{D,E} \ {A} = {D,E}
by A6, A7, ZFMISC_1:72;
{B,C,D,E,F,J} \ {A} =
({B} \/ {C,D,E,F,J}) \ {A}
by ENUMSET1:51
.=
({B} \ {A}) \/ ({C,D,E,F,J} \ {A})
by XBOOLE_1:42
.=
{B} \/ ({C,D,E,F,J} \ {A})
by A4, ZFMISC_1:67
.=
{B} \/ (({C} \/ {D,E,F,J}) \ {A})
by ENUMSET1:47
.=
{B} \/ (({C} \ {A}) \/ ({D,E,F,J} \ {A}))
by XBOOLE_1:42
.=
{B} \/ (({C} \ {A}) \/ (({D,E} \/ {F,J}) \ {A}))
by ENUMSET1:45
.=
{B} \/ (({C} \ {A}) \/ (({D,E} \ {A}) \/ ({F,J} \ {A})))
by XBOOLE_1:42
.=
{B} \/ (({C} \ {A}) \/ ({D,E} \/ {F,J}))
by A8, A9, A10, ZFMISC_1:72
.=
{B} \/ ({C} \/ ({D,E} \/ {F,J}))
by A5, ZFMISC_1:67
.=
{B} \/ ({C} \/ {D,E,F,J})
by ENUMSET1:45
.=
{B} \/ {C,D,E,F,J}
by ENUMSET1:47
.=
{B,C,D,E,F,J}
by ENUMSET1:51
;
then A11: G \ {A} =
({A} \ {A}) \/ {B,C,D,E,F,J}
by A3, XBOOLE_1:42
.=
{} \/ {B,C,D,E,F,J}
by XBOOLE_1:37
;
A12:
((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J c= '/\' (G \ {A})
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J or x in '/\' (G \ {A}) )
assume A13:
x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
;
:: thesis: x in '/\' (G \ {A})
then
x in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E) '/\' F),J) \ {{} }
by PARTIT1:def 4;
then consider bcdef,
j being
set such that A14:
(
bcdef in (((B '/\' C) '/\' D) '/\' E) '/\' F &
j in J &
x = bcdef /\ j )
by SETFAM_1:def 5;
bcdef in (INTERSECTION (((B '/\' C) '/\' D) '/\' E),F) \ {{} }
by A14, PARTIT1:def 4;
then consider bcde,
f being
set such that A15:
(
bcde in ((B '/\' C) '/\' D) '/\' E &
f in F &
bcdef = bcde /\ f )
by SETFAM_1:def 5;
bcde in (INTERSECTION ((B '/\' C) '/\' D),E) \ {{} }
by A15, PARTIT1:def 4;
then consider bcd,
e being
set such that A16:
(
bcd in (B '/\' C) '/\' D &
e in E &
bcde = bcd /\ e )
by SETFAM_1:def 5;
bcd in (INTERSECTION (B '/\' C),D) \ {{} }
by A16, PARTIT1:def 4;
then consider bc,
d being
set such that A17:
(
bc in B '/\' C &
d in D &
bcd = bc /\ d )
by SETFAM_1:def 5;
bc in (INTERSECTION B,C) \ {{} }
by A17, PARTIT1:def 4;
then consider b,
c being
set such that A18:
(
b in B &
c in C &
bc = b /\ c )
by SETFAM_1:def 5;
set h =
(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j);
A19:
dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) =
{J,B,C,D,E,F}
by Th41
.=
{J} \/ {B,C,D,E,F}
by ENUMSET1:51
.=
{B,C,D,E,F,J}
by ENUMSET1:55
;
A20:
dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) =
{J,B,C,D,E,F}
by Th41
.=
{J} \/ {B,C,D,E,F}
by ENUMSET1:51
.=
{B,C,D,E,F,J}
by ENUMSET1:55
;
A21:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D = d
by A1, Th40;
A22:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B = b
by A1, Th40;
A23:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C = c
by A1, Th40;
A24:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E = e
by A1, Th40;
A25:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F = f
by A1, Th40;
A26:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J = j
by A1, Th40;
A27:
for
p being
set st
p in G \ {A} holds
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . p in p
D in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A20, ENUMSET1:def 4;
then A28:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 5;
B in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A20, ENUMSET1:def 4;
then A29:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 5;
C in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A20, ENUMSET1:def 4;
then A30:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 5;
E in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A20, ENUMSET1:def 4;
then A31:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 5;
F in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A20, ENUMSET1:def 4;
then A32:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 5;
J in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A20, ENUMSET1:def 4;
then A33:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 5;
A34:
rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) c= {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)}
proof
let t be
set ;
:: according to TARSKI:def 3 :: thesis: ( not t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) or t in {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)} )
assume
t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
;
:: thesis: t in {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)}
then consider x1 being
set such that A35:
(
x1 in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) &
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . x1 )
by FUNCT_1:def 5;
(
x1 = B or
x1 = C or
x1 = D or
x1 = E or
x1 = F or
x1 = J )
by A20, A35, ENUMSET1:def 4;
hence
t in {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)}
by A35, ENUMSET1:def 4;
:: thesis: verum
end;
{(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)} c= rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
proof
let t be
set ;
:: according to TARSKI:def 3 :: thesis: ( not t in {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)} or t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) )
assume
t in {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)}
;
:: thesis: t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
hence
t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A28, A29, A30, A31, A32, A33, ENUMSET1:def 4;
:: thesis: verum
end;
then A36:
rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) = {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)}
by A34, XBOOLE_0:def 10;
rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) c= bool Y
proof
let t be
set ;
:: according to TARSKI:def 3 :: thesis: ( not t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) or t in bool Y )
assume
t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
;
:: thesis: t in bool Y
then
(
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D or
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B or
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C or
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E or
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F or
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J )
by A34, ENUMSET1:def 4;
hence
t in bool Y
by A14, A15, A16, A17, A18, A21, A22, A23, A24, A25, A26;
:: thesis: verum
end;
then reconsider FF =
rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) as
Subset-Family of
Y ;
reconsider h =
(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j) as
Function ;
A37:
Intersect FF = meet (rng h)
by A28, SETFAM_1:def 10;
A38:
x c= Intersect FF
Intersect FF c= x
proof
let t be
set ;
:: according to TARSKI:def 3 :: thesis: ( not t in Intersect FF or t in x )
assume A46:
t in Intersect FF
;
:: thesis: t in x
(
h . B in rng h &
h . C in rng h &
h . D in rng h &
h . E in rng h &
h . F in rng h &
h . J in rng h )
by A36, ENUMSET1:def 4;
then A47:
(
t in b &
t in c &
t in d &
t in e &
t in f &
t in j )
by A21, A22, A23, A24, A25, A26, A37, A46, SETFAM_1:def 1;
then
t in b /\ c
by XBOOLE_0:def 4;
then
t in (b /\ c) /\ d
by A47, XBOOLE_0:def 4;
then
t in ((b /\ c) /\ d) /\ e
by A47, XBOOLE_0:def 4;
then
t in (((b /\ c) /\ d) /\ e) /\ f
by A47, XBOOLE_0:def 4;
hence
t in x
by A14, A15, A16, A17, A18, A47, XBOOLE_0:def 4;
:: thesis: verum
end;
then A48:
x = Intersect FF
by A38, XBOOLE_0:def 10;
x <> {}
by A13, EQREL_1:def 6;
hence
x in '/\' (G \ {A})
by A11, A19, A27, A48, BVFUNC_2:def 1;
:: thesis: verum
end;
'/\' (G \ {A}) c= ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in '/\' (G \ {A}) or x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J )
assume
x in '/\' (G \ {A})
;
:: thesis: x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
then consider h being
Function,
FF being
Subset-Family of
Y such that A49:
(
dom h = G \ {A} &
rng h = FF & ( for
d being
set st
d in G \ {A} holds
h . d in d ) &
x = Intersect FF &
x <> {} )
by BVFUNC_2:def 1;
A50:
(
B in G \ {A} &
C in G \ {A} &
D in G \ {A} &
E in G \ {A} &
F in G \ {A} &
J in G \ {A} )
by A11, ENUMSET1:def 4;
then A51:
(
h . B in B &
h . C in C &
h . D in D &
h . E in E &
h . F in F &
h . J in J )
by A49;
A52:
(
h . B in rng h &
h . C in rng h &
h . D in rng h &
h . E in rng h &
h . F in rng h &
h . J in rng h )
by A49, A50, FUNCT_1:def 5;
then A53:
Intersect FF = meet (rng h)
by A49, SETFAM_1:def 10;
A54:
not
x in {{} }
by A49, TARSKI:def 1;
A55:
(((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) c= x
proof
let m be
set ;
:: according to TARSKI:def 3 :: thesis: ( not m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) or m in x )
assume A56:
m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)
;
:: thesis: m in x
then
(
m in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) &
m in h . J )
by XBOOLE_0:def 4;
then A57:
(
m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) &
m in h . F )
by XBOOLE_0:def 4;
then
(
m in ((h . B) /\ (h . C)) /\ (h . D) &
m in h . E &
m in h . F )
by XBOOLE_0:def 4;
then
(
m in (h . B) /\ (h . C) &
m in h . D )
by XBOOLE_0:def 4;
then A58:
(
m in h . B &
m in h . C &
m in h . D &
m in h . E &
m in h . F &
m in h . J )
by A56, A57, XBOOLE_0:def 4;
rng h c= {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
proof
let u be
set ;
:: according to TARSKI:def 3 :: thesis: ( not u in rng h or u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)} )
assume
u in rng h
;
:: thesis: u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
then consider x1 being
set such that A59:
(
x1 in dom h &
u = h . x1 )
by FUNCT_1:def 5;
(
x1 = B or
x1 = C or
x1 = D or
x1 = E or
x1 = F or
x1 = J )
by A11, A49, A59, ENUMSET1:def 4;
hence
u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
by A59, ENUMSET1:def 4;
:: thesis: verum
end;
then
for
y being
set st
y in rng h holds
m in y
by A58, ENUMSET1:def 4;
hence
m in x
by A49, A52, A53, SETFAM_1:def 1;
:: thesis: verum
end;
A60:
x c= (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)
then A62:
(((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) = x
by A55, XBOOLE_0:def 10;
set mbc =
(h . B) /\ (h . C);
set mbcd =
((h . B) /\ (h . C)) /\ (h . D);
set mbcde =
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E);
set mbcdef =
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F);
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) <> {}
by A49, A60;
then A63:
not
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in {{} }
by TARSKI:def 1;
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) <> {}
by A49, A60;
then A64:
not
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in {{} }
by TARSKI:def 1;
((h . B) /\ (h . C)) /\ (h . D) <> {}
by A49, A60;
then A65:
not
((h . B) /\ (h . C)) /\ (h . D) in {{} }
by TARSKI:def 1;
(h . B) /\ (h . C) <> {}
by A49, A60;
then A66:
not
(h . B) /\ (h . C) in {{} }
by TARSKI:def 1;
(h . B) /\ (h . C) in INTERSECTION B,
C
by A51, SETFAM_1:def 5;
then
(h . B) /\ (h . C) in (INTERSECTION B,C) \ {{} }
by A66, 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 A51, SETFAM_1:def 5;
then
((h . B) /\ (h . C)) /\ (h . D) in (INTERSECTION (B '/\' C),D) \ {{} }
by A65, XBOOLE_0:def 5;
then
((h . B) /\ (h . C)) /\ (h . D) in (B '/\' C) '/\' D
by PARTIT1:def 4;
then
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in INTERSECTION ((B '/\' C) '/\' D),
E
by A51, SETFAM_1:def 5;
then
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in (INTERSECTION ((B '/\' C) '/\' D),E) \ {{} }
by A64, XBOOLE_0:def 5;
then
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in ((B '/\' C) '/\' D) '/\' E
by PARTIT1:def 4;
then
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in INTERSECTION (((B '/\' C) '/\' D) '/\' E),
F
by A51, SETFAM_1:def 5;
then
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in (INTERSECTION (((B '/\' C) '/\' D) '/\' E),F) \ {{} }
by A63, XBOOLE_0:def 5;
then
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in (((B '/\' C) '/\' D) '/\' E) '/\' F
by PARTIT1:def 4;
then
x in INTERSECTION ((((B '/\' C) '/\' D) '/\' E) '/\' F),
J
by A51, A62, SETFAM_1:def 5;
then
x in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E) '/\' F),J) \ {{} }
by A54, XBOOLE_0:def 5;
hence
x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
by PARTIT1:def 4;
:: thesis: verum
end;
hence
CompF A,G = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
by A2, A12, XBOOLE_0:def 10; :: thesis: verum