let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N & EqClass z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D, E, F, J, M, N being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N & EqClass z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let A, B, C, D, E, F, J, M, N be a_partition of Y; :: thesis: for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N & EqClass z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let z, u be Element of Y; :: thesis: ( G is independent & G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N & EqClass z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) implies EqClass u,(CompF A,G) meets EqClass z,(CompF B,G) )
assume that
A1:
G is independent
and
A2:
( G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N & EqClass z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) )
; :: thesis: EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
A3:
CompF A,G = ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
by A2, Th35;
A4:
CompF B,G = ((((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
by A2, Th36;
reconsider HH = EqClass z,(CompF B,G) as set ;
reconsider I = EqClass z,A as set ;
set GG = EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N);
set h = ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A));
A5:
dom (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) = G
by A2, Th45;
A6:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . A = EqClass z,A
by A2, Th44;
A7:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . B = EqClass u,B
by A2, Th44;
A8:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . C = EqClass u,C
by A2, Th44;
A9:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . D = EqClass u,D
by A2, Th44;
A10:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . E = EqClass u,E
by A2, Th44;
A11:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . F = EqClass u,F
by A2, Th44;
A12:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . J = EqClass u,J
by A2, Th44;
A13:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . M = EqClass u,M
by A2, Th44;
A14:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . N = EqClass u,N
by A2, Th44;
A15:
for d being set st d in G holds
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . d in d
proof
let d be
set ;
:: thesis: ( d in G implies (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . d in d )
assume
d in G
;
:: thesis: (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . d in d
then
(
d = A or
d = B or
d = C or
d = D or
d = E or
d = F or
d = J or
d = M or
d = N )
by A2, ENUMSET1:def 7;
hence
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . d in d
by A6, A7, A8, A9, A10, A11, A12, A13, A14;
:: thesis: verum
end;
A in dom (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by A2, A5, ENUMSET1:def 7;
then A16:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . A in rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
B in dom (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by A2, A5, ENUMSET1:def 7;
then A17:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . B in rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
C in dom (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by A2, A5, ENUMSET1:def 7;
then A18:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . C in rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
D in dom (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by A2, A5, ENUMSET1:def 7;
then A19:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . D in rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
E in dom (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by A2, A5, ENUMSET1:def 7;
then A20:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . E in rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
F in dom (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by A2, A5, ENUMSET1:def 7;
then A21:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . F in rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
J in dom (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by A2, A5, ENUMSET1:def 7;
then A22:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . J in rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
M in dom (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by A2, A5, ENUMSET1:def 7;
then A23:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . M in rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
N in dom (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by A2, A5, ENUMSET1:def 7;
then A24:
(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . N in rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
by FUNCT_1:def 5;
A25:
rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) = {((((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . A),((((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . B),((((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . C),((((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . D),((((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . E),((((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . F),((((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . J),((((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . M),((((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . N)}
by Th46;
rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) c= bool Y
proof
let t be
set ;
:: according to TARSKI:def 3 :: thesis: ( not t in rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) or t in bool Y )
assume
t in rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A)))
;
:: thesis: t in bool Y
then
(
t = (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . A or
t = (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . B or
t = (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . C or
t = (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . D or
t = (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . E or
t = (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . F or
t = (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . J or
t = (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . M or
t = (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) . N )
by A25, ENUMSET1:def 7;
hence
t in bool Y
by A6, A7, A8, A9, A10, A11, A12, A13, A14;
:: thesis: verum
end;
then reconsider FF = rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))) as Subset-Family of Y ;
A26:
Intersect FF = meet (rng (((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (N .--> (EqClass u,N))) +* (A .--> (EqClass z,A))))
by A16, SETFAM_1:def 10;
Intersect FF <> {}
by A1, A5, A15, BVFUNC_2:def 5;
then consider m being set such that
A27:
m in Intersect FF
by XBOOLE_0:def 1;
A28:
( m in EqClass z,A & m in EqClass u,B & m in EqClass u,C & m in EqClass u,D & m in EqClass u,E & m in EqClass u,F & m in EqClass u,J & m in EqClass u,M & m in EqClass u,N )
by A6, A7, A8, A9, A10, A11, A12, A13, A14, A16, A17, A18, A19, A20, A21, A22, A23, A24, A26, A27, SETFAM_1:def 1;
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = (EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) /\ (EqClass u,N)
by Th1;
then
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = ((EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J)) /\ (EqClass u,M)) /\ (EqClass u,N)
by Th1;
then
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = (((EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) /\ (EqClass u,J)) /\ (EqClass u,M)) /\ (EqClass u,N)
by Th1;
then
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = ((((EqClass u,(((B '/\' C) '/\' D) '/\' E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M)) /\ (EqClass u,N)
by Th1;
then
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = (((((EqClass u,((B '/\' C) '/\' D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M)) /\ (EqClass u,N)
by Th1;
then
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = ((((((EqClass u,(B '/\' C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M)) /\ (EqClass u,N)
by Th1;
then A29:
(EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ I = ((((((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M)) /\ (EqClass u,N)) /\ (EqClass z,A)
by Th1;
m in (EqClass u,B) /\ (EqClass u,C)
by A28, XBOOLE_0:def 4;
then
m in ((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)
by A28, XBOOLE_0:def 4;
then
m in (((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)
by A28, XBOOLE_0:def 4;
then
m in ((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)
by A28, XBOOLE_0:def 4;
then
m in (((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)
by A28, XBOOLE_0:def 4;
then
m in ((((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M)
by A28, XBOOLE_0:def 4;
then
m in (((((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M)) /\ (EqClass u,N)
by A28, XBOOLE_0:def 4;
then
(EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ I <> {}
by A28, A29, XBOOLE_0:def 4;
then consider p being set such that
A30:
p in (EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ I
by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A30;
set K = EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N);
A31:
( p in EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) & EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) in (((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N )
by EQREL_1:def 8;
( p in EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) & p in I )
by A30, XBOOLE_0:def 4;
then A32:
p in I /\ (EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))
by A31, XBOOLE_0:def 4;
then
( I /\ (EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) in INTERSECTION A,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) & not I /\ (EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) in {{} } )
by SETFAM_1:def 5, TARSKI:def 1;
then A33:
I /\ (EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) in (INTERSECTION A,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) \ {{} }
by XBOOLE_0:def 5;
set L = EqClass z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N);
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,((((((B '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)
by PARTIT1:16;
then
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,(((((B '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J) '/\' M) '/\' N)
by PARTIT1:16;
then
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,((((B '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J) '/\' M) '/\' N)
by PARTIT1:16;
then
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,(((B '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J)) '/\' M) '/\' N)
by PARTIT1:16;
then
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,((B '/\' (((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) '/\' N)
by PARTIT1:16;
then
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,(B '/\' ((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))
by PARTIT1:16;
then A34:
EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) c= EqClass z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)
by A2, BVFUNC11:3;
A35:
p in EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)
by A30, XBOOLE_0:def 4;
p in EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)
by EQREL_1:def 8;
then
EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) meets EqClass z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)
by A34, A35, XBOOLE_0:3;
then
EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)
by EQREL_1:50;
then A36:
z in EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)
by EQREL_1:def 8;
z in I
by EQREL_1:def 8;
then A37:
z in I /\ (EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))
by A36, XBOOLE_0:def 4;
z in HH
by EQREL_1:def 8;
then A38:
I /\ (EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) meets HH
by A37, XBOOLE_0:3;
A '/\' ((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) =
(A '/\' (((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) '/\' N
by PARTIT1:16
.=
((A '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J)) '/\' M) '/\' N
by PARTIT1:16
.=
(((A '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J) '/\' M) '/\' N
by PARTIT1:16
.=
((((A '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J) '/\' M) '/\' N
by PARTIT1:16
.=
(((((A '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
by PARTIT1:16
.=
((((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
by PARTIT1:16
;
then
I /\ (EqClass p,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) in CompF B,G
by A4, A33, PARTIT1:def 4;
then
p in HH
by A32, A38, EQREL_1:def 6;
hence
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
by A3, A35, XBOOLE_0:3; :: thesis: verum