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