Copyright (c) 1999 Association of Mizar Users
environ
vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, BVFUNC_2, BOOLE, SETFAM_1,
CAT_1, FUNCT_4, RELAT_1, FUNCT_1, CANTOR_1, T_1TOPSP, TARSKI;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
FUNCT_1, FRAENKEL, CQC_LANG, FUNCT_4, MARGREL1, EQREL_1, PARTIT1,
CANTOR_1, BVFUNC_1, BVFUNC_2;
constructors BVFUNC_2, SETWISEO, CANTOR_1, FUNCT_7, BVFUNC_1;
clusters SUBSET_1, PARTIT1, CQC_LANG, MARGREL1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI;
theorems EQREL_1, ZFMISC_1, T_1TOPSP, PARTIT1, BVFUNC_2, BVFUNC11, BVFUNC14,
FUNCT_4, CQC_LANG, TARSKI, ENUMSET1, FUNCT_1, CANTOR_1, SETFAM_1,
BVFUNC23, YELLOW14, XBOOLE_0, XBOOLE_1;
schemes ENUMSET1, XBOOLE_0;
begin :: Chap. 1 Preliminaries
reserve Y for non empty set,
G for Subset of PARTITIONS(Y),
A, B, C, D, E, F, J, M for a_partition of Y,
x,x1,x2,x3,x4,x5,x6,x7,x8,x9,y,X for set;
theorem Th1:
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
proof
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;
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;
assume A13:x in B '/\' C '/\' D '/\' E '/\' F '/\' J;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F,J) \ {{}}
by PARTIT1:def 4;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F,J) & not x in {{}}
by XBOOLE_0: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 bcdef in INTERSECTION(B '/\' C '/\' D '/\' E,F) & not bcdef in {{}}
by XBOOLE_0: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 bcde in INTERSECTION(B '/\' C '/\' D,E) &
not bcde in {{}} by XBOOLE_0: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 bcd in INTERSECTION(B '/\' C,D) & not bcd in {{}} by XBOOLE_0: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 bc in INTERSECTION(B,C) & not bc in {{}} by XBOOLE_0: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 BVFUNC23:8
.= {J} \/ {B,C,D,E,F} by ENUMSET1:51
.= {B,C,D,E,F,J} by ENUMSET1:55;
A20: dom h = {J,B,C,D,E,F} by BVFUNC23:8
.= {J} \/ {B,C,D,E,F} by ENUMSET1:51
.= {B,C,D,E,F,J} by ENUMSET1:55;
A21: h.D = d by A1,BVFUNC23:7;
A22: h.B = b by A1,BVFUNC23:7;
A23: h.C = c by A1,BVFUNC23:7;
A24: h.E = e by A1,BVFUNC23:7;
A25: h.F = f by A1,BVFUNC23:7;
A26: h.J = j by A1,BVFUNC23:7;
A27: for p being set st p in (G \ {A}) holds h.p in p
proof
let p be set;
assume p in (G \ {A});
then p=B or p=C or p=D or p=E or p=F or p=J by A11,ENUMSET1:28;
hence thesis by A1,A14,A15,A16,A17,A18,BVFUNC23:7;
end;
D in dom h by A20,ENUMSET1:29;
then A28: h.D in rng h by FUNCT_1:def 5;
B in dom h by A20,ENUMSET1:29;
then A29: h.B in rng h by FUNCT_1:def 5;
C in dom h by A20,ENUMSET1:29;
then A30: h.C in rng h by FUNCT_1:def 5;
E in dom h by A20,ENUMSET1:29;
then A31: h.E in rng h by FUNCT_1:def 5;
F in dom h by A20,ENUMSET1:29;
then A32: h.F in rng h by FUNCT_1:def 5;
J in dom h by A20,ENUMSET1:29;
then A33: h.J in rng h by FUNCT_1:def 5;
A34:rng h c= {h.B,h.C,h.D,h.E,h.F,h.J}
proof
let t be set;
assume t in rng h;
then consider x1 being set such that
A35: x1 in dom h & t = 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 A20,A35,ENUMSET1:28;
hence thesis by A35,ENUMSET1:29;
end;
{h.B,h.C,h.D,h.E,h.F,h.J} c= rng h
proof
let t be set;
assume t in {h.B,h.C,h.D,h.E,h.F,h.J};
hence thesis by A28,A29,A30,A31,A32,A33,ENUMSET1:28;
end;
then A36:rng h = {h.B,h.C,h.D,h.E,h.F,h.J} by A34,XBOOLE_0:def 10;
rng h c= bool Y
proof
let t be set;
assume t in rng h;
then t=h.D or t=h.B or t=h.C or t=h.E or t=h.F or t=h.J
by A34,ENUMSET1:28;
hence thesis by A14,A15,A16,A17,A18,A21,A22,A23,A24,A25,A26;
end;
then reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
reconsider h as Function;
A37: Intersect FF = meet (rng h) by A28,CANTOR_1:def 3;
A38:x c= Intersect FF
proof
let u be set;
assume A39:u in x;
A40:FF<>{} by A36,ENUMSET1:29;
for y be set holds y in FF implies u in y
proof
let y be set;
assume
A41: y in FF;
now per cases by A34,A41,ENUMSET1:28;
case
A42: y=h.D;
u in (d /\ ((b /\ c) /\ e)) /\ f /\ j
by A14,A15,A16,A17,A18,A39,XBOOLE_1:16;
then u in (d /\ ((b /\ c) /\ e /\ f)) /\ j by XBOOLE_1:16;
then u in d /\ (((b /\ c) /\ e /\ f) /\ j) by XBOOLE_1:16;
hence thesis by A21,A42,XBOOLE_0:def 3;
case
A43: y=h.B;
u in (c /\ (d /\ b)) /\ e /\ f /\
j by A14,A15,A16,A17,A18,A39,XBOOLE_1:16;
then u in c /\ ((d /\ b) /\ e) /\ f /\ j by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ b) /\ f /\ j by XBOOLE_1:16;
then u in c /\ (((d /\ e) /\ b) /\ f) /\ j by XBOOLE_1:16;
then u in c /\ ((((d /\ e) /\ b) /\ f) /\ j) by XBOOLE_1:16;
then u in c /\ (((d /\ e) /\ (f /\ b)) /\ j) by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ ((f /\ b) /\ j)) by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ (f /\ (j /\ b))) by XBOOLE_1:16;
then u in (c /\ (d /\ e)) /\ (f /\ (j /\ b)) by XBOOLE_1:16;
then u in ((c /\ (d /\ e)) /\ f) /\ (j /\ b) by XBOOLE_1:16;
then u in (((c /\ (d /\ e)) /\ f) /\ j) /\ b by XBOOLE_1:16;
hence thesis by A22,A43,XBOOLE_0:def 3;
case
A44: y=h.C;
u in (c /\ (d /\ b)) /\ e /\ f /\
j by A14,A15,A16,A17,A18,A39,XBOOLE_1:16;
then u in c /\ ((d /\ b) /\ e) /\ f /\ j by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ b) /\ f /\ j by XBOOLE_1:16;
then u in c /\ (((d /\ e) /\ b) /\ f) /\ j by XBOOLE_1:16;
then u in c /\ ((((d /\ e) /\ b) /\ f) /\ j) by XBOOLE_1:16;
hence thesis by A23,A44,XBOOLE_0:def 3;
case
A45: y=h.E;
u in ((b /\ c) /\ d) /\ (f /\ e) /\ j
by A14,A15,A16,A17,A18,A39,XBOOLE_1:16;
then u in ((b /\ c) /\ d) /\ ((f /\ e) /\ j) by XBOOLE_1:16;
then u in ((b /\ c) /\ d) /\ ((f /\ j) /\ e) by XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ (f /\ j)) /\ e by XBOOLE_1:16;
hence thesis by A24,A45,XBOOLE_0:def 3;
case
A46: y=h.F;
u in (((b /\ c) /\ d) /\ e) /\ j /\
f by A14,A15,A16,A17,A18,A39,XBOOLE_1:16;
hence thesis by A25,A46,XBOOLE_0:def 3;
case y=h.J;
hence thesis by A14,A26,A39,XBOOLE_0:def 3;
end;
hence thesis;
end;
then u in meet FF by A40,SETFAM_1:def 1;
hence thesis by A40,CANTOR_1:def 3;
end;
Intersect FF c= x
proof
let t be set;
assume
A47: t in Intersect FF;
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:29;
then A48: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,A47,SETFAM_1:def 1;
then t in b /\ c by XBOOLE_0:def 3;
then t in (b /\ c) /\ d by A48,XBOOLE_0:def 3;
then t in (b /\ c) /\ d /\ e by A48,XBOOLE_0:def 3;
then t in (b /\ c) /\ d /\ e /\ f by A48,XBOOLE_0:def 3;
hence thesis by A14,A15,A16,A17,A18,A48,XBOOLE_0:def 3;
end;
then A49:x = Intersect FF by A38,XBOOLE_0:def 10;
x<>{} by A13,EQREL_1:def 6;
hence thesis by A11,A19,A27,A49,BVFUNC_2:def 1;
end;
'/\' (G \ {A}) c= B '/\' C '/\' D '/\' E '/\' F '/\' J
proof
let x be set;
assume x in '/\' (G \ {A});
then consider h being Function, FF being Subset-Family of Y such that
A50: 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;
A51: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:29;
then A52: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 A50;
A53: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 A50,A51,FUNCT_1:def 5;
then A54:Intersect FF = meet (rng h) by A50,CANTOR_1:def 3;
A55:not (x in {{}}) by A50,TARSKI:def 1;
A56:((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J c= x
proof
let m be set;
assume
A57: m in ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J;
then m in h.B /\ h.C /\ h.D /\ h.E /\ h.F & m in h.J by XBOOLE_0:def 3;
then A58:m in h.B /\ h.C /\ h.D /\ h.E & m in h.F by XBOOLE_0:def 3;
then m in h.B /\ h.C /\ h.D & m in h.E & m in h.F by XBOOLE_0:def 3;
then m in h.B /\ h.C & m in h.D by XBOOLE_0:def 3;
then A59: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 A57,A58,XBOOLE_0:def 3;
rng h c= {h.B,h.C,h.D,h.E,h.F,h.J}
proof
let u be set;
assume u in rng h;
then consider x1 being set such that
A60: 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,A50,A60,ENUMSET1:28;
hence thesis by A60,ENUMSET1:29;
end;
then for y being set holds y in rng h implies m in y
by A59,ENUMSET1:28;
hence thesis by A50,A53,A54,SETFAM_1:def 1;
end;
A61: x c= ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J
proof
let m be set;
assume m in x;
then A62: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 A50,A53,A54,SETFAM_1:def 1;
then m in h.B /\ h.C by XBOOLE_0:def 3;
then m in h.B /\ h.C /\ h.D by A62,XBOOLE_0:def 3;
then m in h.B /\ h.C /\ h.D /\ h.E by A62,XBOOLE_0:def 3;
then m in h.B /\ h.C /\ h.D /\ h.E /\ h.F by A62,XBOOLE_0:def 3;
hence thesis by A62,XBOOLE_0:def 3;
end;
then A63:((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J = x by A56,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;
mbcdef<>{} by A50,A56,A61,XBOOLE_0:def 10;
then A64:not (mbcdef in {{}}) by TARSKI:def 1;
mbcde<>{} by A50,A56,A61,XBOOLE_0:def 10;
then A65:not (mbcde in {{}}) by TARSKI:def 1;
mbcd<>{} by A50,A56,A61,XBOOLE_0:def 10;
then A66:not (mbcd in {{}}) by TARSKI:def 1;
mbc<>{} by A50,A56,A61,XBOOLE_0:def 10;
then A67:not (mbc in {{}}) by TARSKI:def 1;
mbc in INTERSECTION(B,C) by A52,SETFAM_1:def 5;
then mbc in INTERSECTION(B,C) \ {{}} by A67,XBOOLE_0:def 4;
then mbc in B '/\' C by PARTIT1:def 4;
then mbcd in INTERSECTION(B '/\' C,D) by A52,SETFAM_1:def 5;
then mbcd in INTERSECTION(B '/\' C,D) \ {{}} by A66,XBOOLE_0:def 4;
then mbcd in B '/\' C '/\' D by PARTIT1:def 4;
then mbcde in INTERSECTION(B '/\' C '/\' D,E) by A52,SETFAM_1:def 5;
then mbcde in INTERSECTION(B '/\' C '/\' D,E) \ {{}} by A65,XBOOLE_0:def 4
;
then mbcde in (B '/\' C '/\' D '/\' E) by PARTIT1:def 4;
then mbcdef in INTERSECTION(B '/\' C '/\' D '/\' E,F) by A52,SETFAM_1:def 5
;
then mbcdef in INTERSECTION(B '/\' C '/\' D '/\' E,F) \ {{}}
by A64,XBOOLE_0:def 4;
then mbcdef in (B '/\' C '/\' D '/\' E '/\' F) by PARTIT1:def 4;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F,J)
by A52,A63,SETFAM_1:def 5;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F,J) \ {{}}
by A55,XBOOLE_0:def 4;
hence thesis by PARTIT1:def 4;
end;
hence thesis by A2,A12,XBOOLE_0:def 10;
end;
theorem Th2:
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(B,G) = A '/\' C '/\' D '/\' E '/\' F '/\' J
proof
{A,B,C,D,E,F,J}={A,B} \/ {C,D,E,F,J} by ENUMSET1:57
.={B,A,C,D,E,F,J} by ENUMSET1:57;
hence thesis by Th1;
end;
theorem Th3:
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(C,G) = A '/\' B '/\' D '/\' E '/\' F '/\' J
proof
{A,B,C,D,E,F,J}={A,B,C} \/ {D,E,F,J} by ENUMSET1:58
.={A} \/ {B,C} \/ {D,E,F,J} by ENUMSET1:42
.={A,C,B} \/ {D,E,F,J} by ENUMSET1:42
.={A,C} \/ {B} \/ {D,E,F,J} by ENUMSET1:43
.={C,A,B} \/ {D,E,F,J} by ENUMSET1:43
.={C,A,B,D,E,F,J} by ENUMSET1:58;
hence thesis by Th1;
end;
theorem Th4:
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(D,G) = A '/\' B '/\' C '/\' E '/\' F '/\' J
proof
{A,B,C,D,E,F,J}={A,B} \/ {C,D,E,F,J} by ENUMSET1:57
.={A,B} \/ ({C,D} \/ {E,F,J}) by ENUMSET1:48
.={A,B} \/ {D,C,E,F,J} by ENUMSET1:48
.={A,B,D,C,E,F,J} by ENUMSET1:57;
hence thesis by Th3;
end;
theorem Th5:
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(E,G) = A '/\' B '/\' C '/\' D '/\' F '/\' J
proof
{A,B,C,D,E,F,J}={A,B,C} \/ {D,E,F,J} by ENUMSET1:58
.={A,B,C} \/ ({D,E} \/ {F,J}) by ENUMSET1:45
.={A,B,C} \/ {E,D,F,J} by ENUMSET1:45
.={A,B,C,E,D,F,J} by ENUMSET1:58;
hence thesis by Th4;
end;
theorem Th6:
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(F,G) = A '/\' B '/\' C '/\' D '/\' E '/\' J
proof
{A,B,C,D,E,F,J}={A,B,C,D} \/ {E,F,J} by ENUMSET1:59
.={A,B,C,D} \/ {F,E,J} by ENUMSET1:99
.={A,B,C,D,F,E,J} by ENUMSET1:59;
hence thesis by Th5;
end;
theorem
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(J,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F
proof
{A,B,C,D,E,F,J}={A,B,C,D,E} \/ {F,J} by ENUMSET1:60
.={A,B,C,D,E,J,F} by ENUMSET1:60;
hence thesis by Th6;
end;
theorem Th8:
for A,B,C,D,E,F,J being set,
h being Function, A',B',C',D',E',F',J' being set st
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 &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(A .--> A')
holds h.A = A' & h.B = B' & h.C = C' &
h.D = D' & h.E = E' & h.F = F' &
h.J = J'
proof
let A,B,C,D,E,F,J be set;
let h be Function;
let A',B',C',D',E',F',J' be set;
assume A1:
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 &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(A .--> A');
A2: dom (A .--> A') = {A} by CQC_LANG:5;
A3: h.A = A'
proof
A in dom (A .--> A') by A2,TARSKI:def 1;
then h.A = (A .--> A').A by A1,FUNCT_4:14;
hence thesis by CQC_LANG:6;
end;
A4: h.B = B'
proof
not B in dom (A .--> A') by A1,A2,TARSKI:def 1;
hence h.B=((B .--> B') +* (C .--> C') +*
(D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J')).B by A1,FUNCT_4:12
.= B' by A1,BVFUNC23:7;
end;
A5: h.C = C'
proof
not C in dom (A .--> A') by A1,A2,TARSKI:def 1;
hence h.C=((B .--> B') +* (C .--> C') +*
(D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J')).C by A1,FUNCT_4:12
.= C' by A1,BVFUNC23:7;
end;
A6: h.D = D'
proof
not D in dom (A .--> A') by A1,A2,TARSKI:def 1;
hence h.D=((B .--> B') +* (C .--> C') +*
(D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J')).D by A1,FUNCT_4:12
.= D' by A1,BVFUNC23:7;
end;
A7: h.E = E'
proof
not E in dom (A .--> A') by A1,A2,TARSKI:def 1;
hence h.E=((B .--> B') +* (C .--> C') +*
(D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J')).E by A1,FUNCT_4:12
.= E' by A1,BVFUNC23:7;
end;
A8: h.F = F'
proof
not F in dom (A .--> A') by A1,A2,TARSKI:def 1;
hence h.F=((B .--> B') +* (C .--> C') +*
(D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J')).F by A1,FUNCT_4:12
.= F' by A1,BVFUNC23:7;
end;
h.J = J'
proof
not J in dom (A .--> A') by A1,A2,TARSKI:def 1;
hence h.J=((B .--> B') +* (C .--> C') +*
(D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J')).J by A1,FUNCT_4:12
.= J' by A1,BVFUNC23:7;
end;
hence thesis by A3,A4,A5,A6,A7,A8;
end;
theorem Th9:
for A,B,C,D,E,F,J being set,
h being Function, A',B',C',D',E',F',J' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +* (A .--> A')
holds dom h = {A,B,C,D,E,F,J}
proof
let A,B,C,D,E,F,J be set;
let h be Function;
let A',B',C',D',E',F',J' be set;
assume A1:
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +* (A .--> A');
A2: dom (A .--> A') = {A} by CQC_LANG:5;
dom h = dom ((B .--> B') +* (C .--> C') +*
(D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J')) \/
dom (A .--> A') by A1,FUNCT_4:def 1
.= {J,B,C,D,E,F} \/ dom (A .--> A') by BVFUNC23:8
.= ({B,C,D,E,F} \/ {J}) \/ {A} by A2,ENUMSET1:51
.= {B,C,D,E,F,J} \/ {A} by ENUMSET1:55
.= {A,B,C,D,E,F,J} by ENUMSET1:56;
hence thesis;
end;
theorem Th10:
for A,B,C,D,E,F,J being set,
h being Function, A',B',C',D',E',F',J' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +* (A .--> A')
holds rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J}
proof
let A,B,C,D,E,F,J be set;
let h be Function;
let A',B',C',D',E',F',J' be set;
assume
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(A .--> A');
then A1: dom h = {A,B,C,D,E,F,J} by Th9;
then A in dom h by ENUMSET1:34;
then A2: h.A in rng h by FUNCT_1:def 5;
B in dom h by A1,ENUMSET1:34;
then A3: h.B in rng h by FUNCT_1:def 5;
C in dom h by A1,ENUMSET1:34;
then A4: h.C in rng h by FUNCT_1:def 5;
D in dom h by A1,ENUMSET1:34;
then A5: h.D in rng h by FUNCT_1:def 5;
E in dom h by A1,ENUMSET1:34;
then A6: h.E in rng h by FUNCT_1:def 5;
F in dom h by A1,ENUMSET1:34;
then A7: h.F in rng h by FUNCT_1:def 5;
J in dom h by A1,ENUMSET1:34;
then A8: h.J in rng h by FUNCT_1:def 5;
A9:rng h c= {h.A,h.B,h.C,h.D,h.E,h.F,h.J}
proof
let t be set;
assume t in rng h;
then consider x1 being set such that
A10: x1 in dom h & t = h.x1 by FUNCT_1:def 5;
x1=A or x1=B or x1=C or x1=D or x1=E or x1=F or x1=J
by A1,A10,ENUMSET1:33;
hence thesis by A10,ENUMSET1:34;
end;
{h.A,h.B,h.C,h.D,h.E,h.F,h.J} c= rng h
proof
let t be set;
assume t in {h.A,h.B,h.C,h.D,h.E,h.F,h.J};
hence thesis by A2,A3,A4,A5,A6,A7,A8,ENUMSET1:33;
end;
hence thesis by A9,XBOOLE_0:def 10;
end;
theorem
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J being a_partition of Y, z,u being Element of Y,
h being Function
st G is independent & 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
EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J) meets EqClass(z,A)
proof
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J be a_partition of Y;
let z,u be Element of Y;
let h be Function;
assume that
A1:G is independent and
A2: 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;
reconsider I=EqClass(z,A) as set;
reconsider GG=EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J) as set;
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)) +*
(A .--> EqClass(z,A));
A3: dom h = G by A2,Th9;
A4: h.A = EqClass(z,A) by A2,Th8;
A5: h.B = EqClass(u,B) by A2,Th8;
A6: h.C = EqClass(u,C) by A2,Th8;
A7: h.D = EqClass(u,D) by A2,Th8;
A8: h.E = EqClass(u,E) by A2,Th8;
A9: h.F = EqClass(u,F) by A2,Th8;
A10: h.J = EqClass(u,J) by A2,Th8;
A11: for d being set st d in G holds h.d in d
proof
let d be set;
assume d in G;
then d=A or d=B or d=C or d=D or d=E or d=F or d=J
by A2,ENUMSET1:33;
hence thesis by A4,A5,A6,A7,A8,A9,A10;
end;
A in dom h by A2,A3,ENUMSET1:34;
then A12: h.A in rng h by FUNCT_1:def 5;
B in dom h by A2,A3,ENUMSET1:34;
then A13: h.B in rng h by FUNCT_1:def 5;
C in dom h by A2,A3,ENUMSET1:34;
then A14: h.C in rng h by FUNCT_1:def 5;
D in dom h by A2,A3,ENUMSET1:34;
then A15: h.D in rng h by FUNCT_1:def 5;
E in dom h by A2,A3,ENUMSET1:34;
then A16: h.E in rng h by FUNCT_1:def 5;
F in dom h by A2,A3,ENUMSET1:34;
then A17: h.F in rng h by FUNCT_1:def 5;
J in dom h by A2,A3,ENUMSET1:34;
then A18: h.J in rng h by FUNCT_1:def 5;
A19:rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J} by Th10;
rng h c= bool Y
proof
let t be set;
assume t in rng h;
then t=h.A or t=h.B or t=h.C or t=h.D or t=h.E or t=h.F or
t=h.J by A19,ENUMSET1:33;
hence thesis by A4,A5,A6,A7,A8,A9,A10;
end;
then reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
A20: Intersect FF = meet (rng h) by A12,CANTOR_1:def 3;
(Intersect FF)<>{} by A1,A3,A11,BVFUNC_2:def 5;
then consider m being set such that
A21: m in Intersect FF by XBOOLE_0:def 1;
A22: 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)
by A4,A5,A6,A7,A8,A9,A10,A12,A13,A14,A15,A16,A17,A18,A20,A21,SETFAM_1:
def 1;
GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F) /\ EqClass(u,J)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E) /\ EqClass(u,F) /\ EqClass(u
,J)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D) /\ EqClass(u,E) /\ EqClass(u,F) /\
EqClass(u,J)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C) /\ EqClass(u,D) /\ EqClass(u,E) /\ EqClass
(u,F)
/\
EqClass(u,J)
by BVFUNC14:1;
then A23: GG /\ I = ((((EqClass(u,B) /\ EqClass(u,C)) /\ EqClass(u,D))
/\ EqClass(u,E)) /\ EqClass(u,F) /\ EqClass(u,J)) /\
EqClass(z,A) by BVFUNC14:1;
m in EqClass(u,B) /\ EqClass(u,C) by A22,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) by A22,XBOOLE_0:
def 3
;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
by A22,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
/\
EqClass(u,F) by A22,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
/\
EqClass(u,F) /\ EqClass(u,J) by A22,XBOOLE_0:def 3;
then m in EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J) /\ EqClass(z,A)
by A22,A23,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 7;
end;
theorem
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J being a_partition of Y, z,u being Element of Y
st G is independent & 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 &
EqClass(z,C '/\' D '/\' E '/\' F '/\' J)=
EqClass(u,C '/\' D '/\' E '/\' F '/\' J)
holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G))
proof
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J be a_partition of Y;
let z,u be Element of Y;
assume that
A1: G is independent and
A2: 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 &
EqClass(z,C '/\' D '/\' E '/\' F '/\' J)=
EqClass(u,C '/\' D '/\' E '/\' F '/\' J);
A3:CompF(A,G) = B '/\' C '/\' D '/\' E '/\' F '/\' J by A2,Th1;
A4:CompF(B,G) = A '/\' C '/\' D '/\' E '/\' F '/\' J by A2,Th2;
reconsider HH=EqClass(z,CompF(B,G)) as set;
reconsider I=EqClass(z,A) as set;
reconsider GG=EqClass(u,(((B '/\' C) '/\' D) '/\' E '/\' F '/\' J))
as set;
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)) +*
(A .--> EqClass(z,A));
A5: dom h = G by A2,Th9;
A6: h.A = EqClass(z,A) by A2,Th8;
A7: h.B = EqClass(u,B) by A2,Th8;
A8: h.C = EqClass(u,C) by A2,Th8;
A9: h.D = EqClass(u,D) by A2,Th8;
A10: h.E = EqClass(u,E) by A2,Th8;
A11: h.F = EqClass(u,F) by A2,Th8;
A12: h.J = EqClass(u,J) by A2,Th8;
A13: for d being set st d in G holds h.d in d
proof
let d be set;
assume d in G;
then d=A or d=B or d=C or d=D or d=E or d=F or d=J by A2,ENUMSET1:33;
hence thesis by A6,A7,A8,A9,A10,A11,A12;
end;
A in dom h by A2,A5,ENUMSET1:34;
then A14: h.A in rng h by FUNCT_1:def 5;
B in dom h by A2,A5,ENUMSET1:34;
then A15: h.B in rng h by FUNCT_1:def 5;
C in dom h by A2,A5,ENUMSET1:34;
then A16: h.C in rng h by FUNCT_1:def 5;
D in dom h by A2,A5,ENUMSET1:34;
then A17: h.D in rng h by FUNCT_1:def 5;
E in dom h by A2,A5,ENUMSET1:34;
then A18: h.E in rng h by FUNCT_1:def 5;
F in dom h by A2,A5,ENUMSET1:34;
then A19: h.F in rng h by FUNCT_1:def 5;
J in dom h by A2,A5,ENUMSET1:34;
then A20: h.J in rng h by FUNCT_1:def 5;
A21:rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J} by Th10;
rng h c= bool Y
proof
let t be set;
assume t in rng h;
then t=h.A or t=h.B or t=h.C or t=h.D or t=h.E or t=h.F or t=h.J
by A21,ENUMSET1:33;
hence thesis by A6,A7,A8,A9,A10,A11,A12;
end;
then reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
A22: Intersect FF = meet (rng h) by A14,CANTOR_1:def 3;
(Intersect FF)<>{} by A1,A5,A13,BVFUNC_2:def 5;
then consider m being set such that
A23: m in Intersect FF by XBOOLE_0:def 1;
A24: 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)
by A6,A7,A8,A9,A10,A11,A12,A14,A15,A16,A17,A18,A19,A20,A22,A23,SETFAM_1
:def 1;
GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F) /\ EqClass(u,J)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E) /\ EqClass(u,F) /\ EqClass(u
,J)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D) /\ EqClass(u,E) /\ EqClass(u,F) /\
EqClass(u,J)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C) /\ EqClass(u,D) /\ EqClass(u,E) /\ EqClass
(u,F)
/\
EqClass(u,J)
by BVFUNC14:1;
then A25: GG /\ I = ((((EqClass(u,B) /\ EqClass(u,C)) /\ EqClass(u,D))
/\
EqClass(u,E)) /\ EqClass(u,F) /\ EqClass(u,J)) /\ EqClass(z,A)
by BVFUNC14:1;
m in EqClass(u,B) /\ EqClass(u,C) by A24,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) by A24,XBOOLE_0:
def 3
;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
by A24,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
/\
EqClass(u,F)
by A24,XBOOLE_0:def 3;
then m in (((EqClass(u,B) /\ EqClass(u,C)) /\ EqClass(u,D)) /\ EqClass(u
,E))
/\
EqClass(u,F) /\ EqClass(u,J)
by A24,XBOOLE_0:def 3;
then A26:GG /\ I <> {} by A24,A25,XBOOLE_0:def 3;
then consider p being set such that
A27: p in GG /\ I by XBOOLE_0:def 1;
GG /\ I in INTERSECTION(A,B '/\' C '/\' D '/\' E '/\' F '/\' J) &
not (GG /\ I in {{}})
by A26,SETFAM_1:def 5,TARSKI:def 1;
then GG /\ I in INTERSECTION(A,B '/\' C '/\' D '/\' E '/\' F '/\' J) \ {
{}}
by XBOOLE_0:def 4;
then GG /\ I in (A '/\' ((((B '/\' C) '/\' D) '/\' E) '/\' F '/\' J))
by PARTIT1:def 4;
then reconsider p as Element of Y by A27;
reconsider K=EqClass(p,C '/\' D '/\' E '/\' F '/\' J) as set;
A28:p in K & K in C '/\' D '/\' E '/\' F '/\' J by T_1TOPSP:def 1;
p in GG & p in I by A27,XBOOLE_0:def 3;
then A29:p in I /\ K by A28,XBOOLE_0:def 3;
then I /\ K in INTERSECTION(A,C '/\' D '/\' E '/\' F '/\' J) &
not (I /\ K in {{}}) by SETFAM_1:def 5,TARSKI:def 1;
then I /\ K in INTERSECTION(A,C '/\' D '/\' E '/\' F '/\' J) \ {{}}
by XBOOLE_0:def 4;
then A30: I /\ K in A '/\' (C '/\' D '/\' E '/\' F '/\' J) by PARTIT1:def 4;
reconsider L=EqClass(z,C '/\' D '/\' E '/\' F '/\' J) as set;
GG = EqClass(u,(((B '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J)
by PARTIT1:16;
then GG = EqClass(u,((B '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J)
by PARTIT1:16;
then GG = EqClass(u,(B '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J)
by PARTIT1:16;
then GG = EqClass(u,B '/\' (C '/\' D '/\' E '/\' F '/\' J)) by PARTIT1:16
;
then A31: GG c= L by A2,BVFUNC11:3;
A32: p in GG by A27,XBOOLE_0:def 3;
p in EqClass(p,C '/\' D '/\' E '/\' F '/\' J) by T_1TOPSP:def 1;
then K meets L by A31,A32,XBOOLE_0:3;
then K=L by T_1TOPSP:9;
then A33:z in K by T_1TOPSP:def 1;
z in I by T_1TOPSP:def 1;
then A34:z in I /\ K by A33,XBOOLE_0:def 3;
z in HH by T_1TOPSP:def 1;
then A35:I /\ K meets HH by A34,XBOOLE_0:3;
A '/\' (C '/\' D '/\' E '/\' F '/\' J)
= A '/\' (C '/\' D '/\' E '/\' F) '/\' J by PARTIT1:16
.= A '/\' (C '/\' D '/\' E) '/\' F '/\' J by PARTIT1:16
.= A '/\' (C '/\' D) '/\' E '/\' F '/\' J by PARTIT1:16
.= A '/\' C '/\' D '/\' E '/\' F '/\' J by PARTIT1:16;
then p in HH by A4,A29,A30,A35,EQREL_1:def 6;
hence thesis by A3,A32,XBOOLE_0:3;
end;
theorem Th13:
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
proof
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;
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;
assume A13:x in B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J,M) \ {{}}
by PARTIT1:def 4;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J,M) & not x in
{{}}
by XBOOLE_0: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 bcdefj in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F,J) &
not bcdefj in {{}}
by XBOOLE_0: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 bcdef in INTERSECTION(B '/\' C '/\' D '/\' E,F) & not bcdef in {{}}
by XBOOLE_0: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 bcde in INTERSECTION(B '/\' C '/\' D,E) &
not bcde in {{}} by XBOOLE_0: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 bcd in INTERSECTION(B '/\' C,D) & not bcd in {{}} by XBOOLE_0: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 bc in INTERSECTION(B,C) & not bc in {{}} by XBOOLE_0: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: h.D = d by A1,Th8;
A22: h.B = b by A1,Th8;
A23: h.C = c by A1,Th8;
A24: h.E = e by A1,Th8;
A25: h.F = f by A1,Th8;
A26: h.J = j by A1,Th8;
A27: h.M = m by A1,Th8;
A28: for p being set st p in (G \ {A}) holds h.p in p
proof
let p be set;
assume p in (G \ {A});
then p=D or p=B or p=C or p=E or p=F or p=J or p=M
by A11,ENUMSET1:33;
hence thesis by A1,A14,A15,A16,A17,A18,A19,Th8;
end;
A29: D in dom h by A20,ENUMSET1:34;
then A30: h.D in rng h by FUNCT_1:def 5;
A31: B in dom h by A20,ENUMSET1:34;
A32: C in dom h by A20,ENUMSET1:34;
A33: E in dom h by A20,ENUMSET1:34;
A34: F in dom h by A20,ENUMSET1:34;
A35: J in dom h by A20,ENUMSET1:34;
A36: M in dom h by A20,ENUMSET1:34;
A37:rng h c= {h.B,h.C,h.D,h.E,h.F,h.J,h.M}
proof
let t be set;
assume t in rng h;
then consider x1 being set such that
A38: x1 in dom h & t = h.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:33;
hence thesis by A38,ENUMSET1:34;
end;
A39: {h.B,h.C,h.D,h.E,h.F,h.J,h.M} c= rng h
proof
let t be set;
assume t in {h.B,h.C,h.D,h.E,h.F,h.J,h.M};
then t=h.D or t=h.B or t=h.C or t=h.E or t=h.F or t=h.J or t=h.M
by ENUMSET1:33;
hence thesis by A29,A31,A32,A33,A34,A35,A36,FUNCT_1:def 5;
end;
then A40:rng h = {h.B,h.C,h.D,h.E,h.F,h.J,h.M} by A37,XBOOLE_0:def 10;
rng h c= bool Y
proof
let t be set;
assume t in rng h;
then t=h.D or t=h.B or t=h.C or t=h.E or t=h.F or t=h.J or t=h.M
by A37,ENUMSET1:33;
hence thesis by A14,A15,A16,A17,A18,A19,A21,A22,A23,A24,A25,A26,A27;
end;
then reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
reconsider h as Function;
A41: Intersect FF = meet (rng h) by A30,CANTOR_1:def 3;
A42:x c= Intersect FF
proof
let u be set;
assume A43:u in x;
A44:FF<>{} by A40,ENUMSET1:34;
for y be set holds y in FF implies u in y
proof
let y be set;
assume A45: y in FF;
now per cases by A37,A45,ENUMSET1:33;
case
A46: y=h.D;
u in (d /\ ((b /\ c) /\ e)) /\ f /\ j /\ m
by A14,A15,A16,A17,A18,A19,A43,XBOOLE_1:16;
then u in (d /\ ((b /\ c) /\ e /\ f)) /\ j /\ m by XBOOLE_1:16;
then u in d /\ (((b /\ c) /\ e /\ f) /\ j) /\ m by XBOOLE_1:16;
then u in d /\ ((((b /\ c) /\ e /\ f) /\ j) /\ m) by XBOOLE_1:16;
hence thesis by A21,A46,XBOOLE_0:def 3;
case
A47: y=h.B;
u in (c /\ (d /\ b)) /\ e /\ f /\ j /\ m
by A14,A15,A16,A17,A18,A19,A43,XBOOLE_1:16;
then u in c /\ ((d /\ b) /\ e) /\ f /\ j /\ m by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ b) /\ f /\ j /\ m by XBOOLE_1:16;
then u in c /\ (((d /\ e) /\ b) /\ f) /\ j /\ m by XBOOLE_1:16;
then u in c /\ ((((d /\ e) /\ b) /\ f) /\ j) /\ m by XBOOLE_1:16;
then u in c /\ (((d /\ e) /\ (f /\ b)) /\ j) /\ m by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ ((f /\ b) /\ j)) /\ m by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ (f /\ (j /\ b))) /\ m by XBOOLE_1:16;
then u in (c /\ (d /\ e)) /\ (f /\ (j /\ b)) /\ m by XBOOLE_1:16;
then u in ((c /\ (d /\ e)) /\ f) /\ (j /\ b) /\ m by XBOOLE_1:16;
then u in (((c /\ (d /\ e)) /\ f) /\ j) /\ b /\ m by XBOOLE_1:16;
then u in (((c /\ (d /\ e)) /\ f) /\ j) /\ m /\ b by XBOOLE_1:16;
hence thesis by A22,A47,XBOOLE_0:def 3;
case
A48: y=h.C;
u in (c /\ (d /\ b)) /\ e /\ f /\ j /\ m
by A14,A15,A16,A17,A18,A19,A43,XBOOLE_1:16;
then u in c /\ ((d /\ b) /\ e) /\ f /\ j /\ m by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ b) /\ f /\ j /\ m by XBOOLE_1:16;
then u in c /\ (((d /\ e) /\ b) /\ f) /\ j /\ m by XBOOLE_1:16;
then u in c /\ ((((d /\ e) /\ b) /\ f) /\ j) /\ m by XBOOLE_1:16;
then u in c /\ (((((d /\ e) /\ b) /\ f) /\ j) /\ m) by XBOOLE_1:16;
hence thesis by A23,A48,XBOOLE_0:def 3;
case
A49: y=h.E;
u in ((b /\ c) /\ d) /\ (f /\ e) /\ j /\ m
by A14,A15,A16,A17,A18,A19,A43,XBOOLE_1:16;
then u in ((b /\ c) /\ d) /\ ((f /\ e) /\ j) /\ m by XBOOLE_1:16;
then u in ((b /\ c) /\ d) /\ ((f /\ j) /\ e) /\ m by XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ (f /\ j)) /\ e /\ m by XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ (f /\ j)) /\ m /\ e by XBOOLE_1:16;
hence thesis by A24,A49,XBOOLE_0:def 3;
case
A50: y=h.F;
u in (((b /\ c) /\ d) /\ e) /\ j /\ f /\ m
by A14,A15,A16,A17,A18,A19,A43,XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ e) /\ j /\ m /\ f by XBOOLE_1:16;
hence thesis by A25,A50,XBOOLE_0:def 3;
case
A51: y=h.J;
u in (((b /\ c) /\ d) /\ e) /\ f /\ m /\ j
by A14,A15,A16,A17,A18,A19,A43,XBOOLE_1:16;
hence thesis by A26,A51,XBOOLE_0:def 3;
case y=h.M;
hence thesis by A14,A27,A43,XBOOLE_0:def 3;
end;
hence thesis;
end;
then u in meet FF by A44,SETFAM_1:def 1;
hence thesis by A44,CANTOR_1:def 3;
end;
Intersect FF c= x
proof
let t be set;
assume
A52: t in Intersect FF;
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:34;
then A53: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,A52,SETFAM_1:def 1;
then t in b /\ c by XBOOLE_0:def 3;
then t in (b /\ c) /\ d by A53,XBOOLE_0:def 3;
then t in (b /\ c) /\ d /\ e by A53,XBOOLE_0:def 3;
then t in (b /\ c) /\ d /\ e /\ f by A53,XBOOLE_0:def 3;
then t in (b /\ c) /\ d /\ e /\ f /\ j by A53,XBOOLE_0:def 3;
hence thesis by A14,A15,A16,A17,A18,A19,A53,XBOOLE_0:def 3;
end;
then A54:x = Intersect FF by A42,XBOOLE_0:def 10;
x<>{} by A13,EQREL_1:def 6;
hence thesis by A11,A20,A28,A54,BVFUNC_2:def 1;
end;
'/\' (G \ {A}) c= B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M
proof
let x be set;
assume x in '/\' (G \ {A});
then consider h being Function, FF being Subset-Family of Y such that
A55: 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;
A56: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:34;
then A57: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 A55;
A58: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 A55,A56,FUNCT_1:def 5;
then A59:Intersect FF = meet (rng h) by A55,CANTOR_1:def 3;
A60:not (x in {{}}) by A55,TARSKI:def 1;
A61:((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J /\ h.M c= x
proof
let p be set;
assume p in ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J /\ h.M;
then A62:p in ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J & p in h.M
by XBOOLE_0:def 3;
then p in h.B /\ h.C /\ h.D /\ h.E /\ h.F & p in h.J by XBOOLE_0:def 3;
then A63:p in h.B /\ h.C /\ h.D /\ h.E & p in h.F by XBOOLE_0:def 3;
then p in h.B /\ h.C /\ h.D & p in h.E & p in h.F by XBOOLE_0:def 3;
then p in h.B /\ h.C & p in h.D by XBOOLE_0:def 3;
then A64: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 A62,A63,XBOOLE_0:def 3;
rng h c= {h.B,h.C,h.D,h.E,h.F,h.J,h.M}
proof
let u be set;
assume u in rng h;
then consider x1 being set such that
A65: 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,A55,A65,ENUMSET1:33;
hence thesis by A65,ENUMSET1:34;
end;
then for y being set holds y in rng h implies p in y
by A64,ENUMSET1:33;
hence thesis by A55,A58,A59,SETFAM_1:def 1;
end;
A66: x c= ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J /\ h.M
proof
let p be set;
assume p in x;
then A67: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 A55,A58,A59,SETFAM_1:def 1;
then p in h.B /\ h.C by XBOOLE_0:def 3;
then p in h.B /\ h.C /\ h.D by A67,XBOOLE_0:def 3;
then p in h.B /\ h.C /\ h.D /\ h.E by A67,XBOOLE_0:def 3;
then p in h.B /\ h.C /\ h.D /\ h.E /\ h.F by A67,XBOOLE_0:def 3;
then p in ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J by A67,XBOOLE_0:
def 3
;
hence thesis by A67,XBOOLE_0:def 3;
end;
then A68:((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J /\ h.M = x
by A61,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;
mbcdefj<>{} by A55,A61,A66,XBOOLE_0:def 10;
then A69:not (mbcdefj in {{}}) by TARSKI:def 1;
mbcdef<>{} by A55,A61,A66,XBOOLE_0:def 10;
then A70:not (mbcdef in {{}}) by TARSKI:def 1;
mbcde<>{} by A55,A61,A66,XBOOLE_0:def 10;
then A71:not (mbcde in {{}}) by TARSKI:def 1;
mbcd<>{} by A55,A61,A66,XBOOLE_0:def 10;
then A72:not (mbcd in {{}}) by TARSKI:def 1;
mbc<>{} by A55,A61,A66,XBOOLE_0:def 10;
then A73:not (mbc in {{}}) by TARSKI:def 1;
mbc in INTERSECTION(B,C) by A57,SETFAM_1:def 5;
then mbc in INTERSECTION(B,C) \ {{}} by A73,XBOOLE_0:def 4;
then mbc in B '/\' C by PARTIT1:def 4;
then mbcd in INTERSECTION(B '/\' C,D) by A57,SETFAM_1:def 5;
then mbcd in INTERSECTION(B '/\' C,D) \ {{}} by A72,XBOOLE_0:def 4;
then mbcd in B '/\' C '/\' D by PARTIT1:def 4;
then mbcde in INTERSECTION(B '/\' C '/\' D,E) by A57,SETFAM_1:def 5;
then mbcde in INTERSECTION(B '/\' C '/\' D,E) \ {{}} by A71,XBOOLE_0:def 4
;
then mbcde in (B '/\' C '/\' D '/\' E) by PARTIT1:def 4;
then mbcdef in INTERSECTION(B '/\' C '/\' D '/\' E,F) by A57,SETFAM_1:def 5
;
then mbcdef in INTERSECTION(B '/\' C '/\' D '/\' E,F) \ {{}}
by A70,XBOOLE_0:def 4;
then mbcdef in (B '/\' C '/\' D '/\' E '/\' F) by PARTIT1:def 4;
then mbcdefj in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F,J)
by A57,SETFAM_1:def 5;
then mbcdefj in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F,J) \ {{}}
by A69,XBOOLE_0:def 4;
then mbcdefj in (B '/\' C '/\' D '/\' E '/\' F '/\' J) by PARTIT1:def 4;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J,M)
by A57,A68,SETFAM_1:def 5;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J,M) \ {{}}
by A60,XBOOLE_0:def 4;
hence thesis by PARTIT1:def 4;
end;
hence thesis by A2,A12,XBOOLE_0:def 10;
end;
theorem Th14:
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(B,G) = A '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M
proof
{A,B,C,D,E,F,J,M}={A,B} \/ {C,D,E,F,J,M} by ENUMSET1:63
.={B,A,C,D,E,F,J,M} by ENUMSET1:63;
hence thesis by Th13;
end;
theorem Th15:
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(C,G) = A '/\' B '/\' D '/\' E '/\' F '/\' J '/\' M
proof
{A,B,C,D,E,F,J,M} ={A,B,C} \/ {D,E,F,J,M} by ENUMSET1:64
.={A} \/ {B,C} \/ {D,E,F,J,M} by ENUMSET1:42
.={A,C,B} \/ {D,E,F,J,M} by ENUMSET1:42
.={A,C,B,D,E,F,J,M} by ENUMSET1:64;
hence thesis by Th14;
end;
theorem Th16:
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(D,G) = A '/\' B '/\' C '/\' E '/\' F '/\' J '/\' M
proof
{A,B,C,D,E,F,J,M} ={A,B} \/ {C,D,E,F,J,M} by ENUMSET1:63
.={A,B} \/ ({C,D} \/ {E,F,J,M}) by ENUMSET1:52
.={A,B} \/ {D,C,E,F,J,M} by ENUMSET1:52
.={A,B,D,C,E,F,J,M} by ENUMSET1:63;
hence thesis by Th15;
end;
theorem Th17:
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(E,G) = A '/\' B '/\' C '/\' D '/\' F '/\' J '/\' M
proof
{A,B,C,D,E,F,J,M} ={A,B,C} \/ {D,E,F,J,M} by ENUMSET1:64
.={A,B,C} \/ ({D,E} \/ {F,J,M}) by ENUMSET1:48
.={A,B,C} \/ ({E,D,F,J,M}) by ENUMSET1:48
.={A,B,C,E,D,F,J,M} by ENUMSET1:64;
hence thesis by Th16;
end;
theorem Th18:
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(F,G) = A '/\' B '/\' C '/\' D '/\' E '/\' J '/\' M
proof
{A,B,C,D,E,F,J,M} ={A,B,C,D} \/ {E,F,J,M} by ENUMSET1:65
.={A,B,C,D} \/ ({E,F} \/ {J,M}) by ENUMSET1:45
.={A,B,C,D} \/ ({F,E,J,M}) by ENUMSET1:45
.={A,B,C,D,F,E,J,M} by ENUMSET1:65;
hence thesis by Th17;
end;
theorem Th19:
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(J,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' M
proof
{A,B,C,D,E,F,J,M} ={A,B,C,D,E} \/ {F,J,M} by ENUMSET1:66
.={A,B,C,D,E} \/ ({J,F} \/ {M}) by ENUMSET1:43
.={A,B,C,D,E} \/ ({J,F,M}) by ENUMSET1:43
.={A,B,C,D,E,J,F,M} by ENUMSET1:66;
hence thesis by Th18;
end;
theorem
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(M,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' J
proof
{A,B,C,D,E,F,J,M} ={A,B,C,D,E,F} \/ {J,M} by ENUMSET1:67
.={A,B,C,D,E,F,M,J} by ENUMSET1:67;
hence thesis by Th19;
end;
theorem Th21:
for A,B,C,D,E,F,J,M being set, h being Function,
A',B',C',D',E',F',J',M' being set st
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 &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(M .--> M') +* (A .--> A')
holds h.B = B' & h.C = C' &
h.D = D' & h.E = E' & h.F = F' &
h.J = J'
proof
let A,B,C,D,E,F,J,M be set;
let h be Function;
let A',B',C',D',E',F',J',M' be set;
assume A1: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 &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +* (M .--> M') +* (A .--> A');
A2: dom (A .--> A') = {A} by CQC_LANG:5;
A3: h.B = B'
proof
not B in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.B=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M')).B by A1,FUNCT_4:12
.= B' by A1,Th8;
hence thesis;
end;
A4: h.C = C'
proof
not C in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.C=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M')).C
by A1,FUNCT_4:12;
hence thesis by A1,Th8;
end;
A5: h.D = D'
proof
not D in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.D=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M')).D by A1,FUNCT_4:12
.= D' by A1,Th8;
hence thesis;
end;
A6: h.E = E'
proof
not E in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.E=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M')).E by A1,FUNCT_4:12
.= E' by A1,Th8;
hence thesis;
end;
A7: h.F = F'
proof
not F in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.F=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M')).F by A1,FUNCT_4:12
.= F' by A1,Th8;
hence thesis;
end;
h.J = J'
proof
not J in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.J=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M')).J by A1,FUNCT_4:12
.= J' by A1,Th8;
hence thesis;
end;
hence thesis by A3,A4,A5,A6,A7;
end;
theorem Th22:
for A,B,C,D,E,F,J,M being set, h being Function,
A',B',C',D',E',F',J',M' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(M .--> M') +* (A .--> A')
holds dom h = {A,B,C,D,E,F,J,M}
proof
let A,B,C,D,E,F,J,M be set;
let h be Function;
let A',B',C',D',E',F',J',M' be set;
assume A1:
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(M .--> M') +* (A .--> A');
A2: 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;
dom (A .--> A') = {A} by CQC_LANG:5;
then dom ((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M') +*(A .--> A'))
= {B,C,D,E,F,J,M} \/ {A} by A2,FUNCT_4:def 1
.= {A,B,C,D,E,F,J,M} by ENUMSET1:62;
hence thesis by A1;
end;
theorem Th23:
for A,B,C,D,E,F,J,M being set, h being Function,
A',B',C',D',E',F',J',M' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(M .--> M') +* (A .--> A')
holds rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M}
proof
let A,B,C,D,E,F,J,M be set;
let h be Function;
let A',B',C',D',E',F',J',M' be set;
assume
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(M .--> M') +* (A .--> A');
then A1: dom h = {A,B,C,D,E,F,J,M} by Th22;
then A in dom h by ENUMSET1:39;
then A2: h.A in rng h by FUNCT_1:def 5;
B in dom h by A1,ENUMSET1:39;
then A3: h.B in rng h by FUNCT_1:def 5;
C in dom h by A1,ENUMSET1:39;
then A4: h.C in rng h by FUNCT_1:def 5;
D in dom h by A1,ENUMSET1:39;
then A5: h.D in rng h by FUNCT_1:def 5;
E in dom h by A1,ENUMSET1:39;
then A6: h.E in rng h by FUNCT_1:def 5;
F in dom h by A1,ENUMSET1:39;
then A7: h.F in rng h by FUNCT_1:def 5;
J in dom h by A1,ENUMSET1:39;
then A8: h.J in rng h by FUNCT_1:def 5;
M in dom h by A1,ENUMSET1:39;
then A9: h.M in rng h by FUNCT_1:def 5;
A10:rng h c= {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M}
proof
let t be set;
assume t in rng h;
then consider x1 being set such that
A11: x1 in dom h & t = h.x1 by FUNCT_1:def 5;
x1=A or x1=B or x1=C or x1=D or x1=E or x1=F or x1=J or x1=M
by A1,A11,ENUMSET1:38;
hence thesis by A11,ENUMSET1:39;
end;
{h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M} c= rng h
proof
let t be set;
assume t in {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M};
hence thesis by A2,A3,A4,A5,A6,A7,A8,A9,ENUMSET1:38;
end;
hence thesis by A10,XBOOLE_0:def 10;
end;
theorem
for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M being a_partition of Y
, z,u being Element of Y, h being Function
st G is independent & 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 EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M) /\
EqClass(z,A) <> {}
proof
let a be Element of Funcs(Y,BOOLEAN);
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M be a_partition of Y;
let z,u be Element of Y;
let h be Function;
assume that
A1:G is independent and
A2: 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;
reconsider I=EqClass(z,A) as set;
reconsider GG=EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M)
as set;
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)) +*
(A .--> EqClass(z,A));
A3: dom h = G by A2,Th22;
A4: h.A = EqClass(z,A) by YELLOW14:3;
A5: h.B = EqClass(u,B) by A2,Th21;
A6: h.C = EqClass(u,C) by A2,Th21;
A7: h.D = EqClass(u,D) by A2,Th21;
A8: h.E = EqClass(u,E) by A2,Th21;
A9: h.F = EqClass(u,F) by A2,Th21;
A10: h.J = EqClass(u,J) by A2,Th21;
A11: h.M = EqClass(u,M) by A2,BVFUNC14:15;
A12: for d being set st d in G holds h.d in d
proof
let d be set;
assume d in G;
then d=A or d=B or d=C or d=D or d=E or d=F or d=J or d=M
by A2,ENUMSET1:38;
hence thesis by A4,A5,A6,A7,A8,A9,A10,A11;
end;
A in dom h by A2,A3,ENUMSET1:39;
then A13: h.A in rng h by FUNCT_1:def 5;
B in dom h by A2,A3,ENUMSET1:39;
then A14: h.B in rng h by FUNCT_1:def 5;
C in dom h by A2,A3,ENUMSET1:39;
then A15: h.C in rng h by FUNCT_1:def 5;
D in dom h by A2,A3,ENUMSET1:39;
then A16: h.D in rng h by FUNCT_1:def 5;
E in dom h by A2,A3,ENUMSET1:39;
then A17: h.E in rng h by FUNCT_1:def 5;
F in dom h by A2,A3,ENUMSET1:39;
then A18: h.F in rng h by FUNCT_1:def 5;
J in dom h by A2,A3,ENUMSET1:39;
then A19: h.J in rng h by FUNCT_1:def 5;
M in dom h by A2,A3,ENUMSET1:39;
then A20: h.M in rng h by FUNCT_1:def 5;
A21:rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M} by Th23;
rng h c= bool Y
proof
let t be set;
assume t in rng h;
then t=h.A or t=h.B or t=h.C or t=h.D or t=h.E or t=h.F or
t=h.J or t=h.M by A21,ENUMSET1:38;
hence thesis by A4,A5,A6,A7,A8,A9,A10,A11;
end;
then reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
A22: Intersect FF = meet (rng h) by A13,CANTOR_1:def 3;
(Intersect FF)<>{} by A1,A3,A12,BVFUNC_2:def 5;
then consider m being set such that
A23: m in Intersect FF by XBOOLE_0:def 1;
A24: 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)
by A4,A5,A6,A7,A8,A9,A10,A11,A13,A14,A15,A16,A17,A18,A19,A20,A22,A23,
SETFAM_1:def 1;
GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J) /\ EqClass(u,M)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F) /\ EqClass(u,J) /\
EqClass(u,M)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E) /\ EqClass(u,F) /\ EqClass(u
,J) /\
EqClass(u,M)
by BVFUNC14:1;
then GG = (EqClass(u,B '/\' C '/\' D) /\ EqClass(u,E)) /\ EqClass(u,F)
/\
EqClass(u,J) /\ EqClass(u,M)
by BVFUNC14:1;
then GG = ((((EqClass(u,B '/\' C) /\ EqClass(u,D)) /\ EqClass(u,E)) /\
EqClass(u,F)) /\ EqClass(u,J)) /\ EqClass(u,M)
by BVFUNC14:1;
then A25: GG /\ I = ((((EqClass(u,B) /\ EqClass(u,C)) /\ EqClass(u,D))
/\ EqClass(u,E)) /\ EqClass(u,F) /\ EqClass(u,J) /\
EqClass(u,M))
/\ EqClass(z,A) by BVFUNC14:1;
m in EqClass(u,B) /\ EqClass(u,C) by A24,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) by A24,XBOOLE_0:
def 3
;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
by A24,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
/\
EqClass(u,F)
by A24,XBOOLE_0:def 3;
then m in ((EqClass(u,B) /\ EqClass(u,C)) /\ EqClass(u,D)) /\ EqClass(u,
E)
/\ EqClass(u,F) /\ EqClass(u,J)
by A24,XBOOLE_0:def 3;
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 A24,XBOOLE_0:def 3;
hence thesis by A24,A25,XBOOLE_0:def 3;
end;
theorem
for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M being a_partition of Y
, z,u being Element of Y
st G is independent & 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 &
EqClass(z,C '/\' D '/\' E '/\' F '/\' J '/\' M)=
EqClass(u,C '/\' D '/\' E '/\' F '/\' J '/\' M)
holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G))
proof
let a be Element of Funcs(Y,BOOLEAN);
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M be a_partition of Y;
let z,u be Element of Y;
assume that
A1:G is independent and
A2: 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 &
EqClass(z,C '/\' D '/\' E '/\' F '/\' J '/\' M)=
EqClass(u,C '/\' D '/\' E '/\' F '/\' J '/\' M);
A3:CompF(B,G) = A '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M
by A2,Th14;
set HH=EqClass(z,CompF(B,G)),
I=EqClass(z,A),
GG=EqClass(u,(((B '/\' C) '/\' D) '/\' E '/\' F '/\' J '/\' M));
A4: GG=EqClass(u,CompF(A,G)) by A2,Th13;
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)) +*
(A .--> EqClass(z,A));
A5: dom h = G by A2,Th22;
A6: h.A = EqClass(z,A) by YELLOW14:3;
A7: h.B = EqClass(u,B) by A2,Th21;
A8: h.C = EqClass(u,C) by A2,Th21;
A9: h.D = EqClass(u,D) by A2,Th21;
A10: h.E = EqClass(u,E) by A2,Th21;
A11: h.F = EqClass(u,F) by A2,Th21;
A12: h.J = EqClass(u,J) by A2,Th21;
A13: h.M = EqClass(u,M) by A2,BVFUNC14:15;
A14: for d being set st d in G holds h.d in d
proof
let d be set;
assume d in G;
then d=A or d=B or d=C or d=D or d=E or d=F or d=J or d=M
by A2,ENUMSET1:38;
hence thesis by A6,A7,A8,A9,A10,A11,A12,A13;
end;
A in dom h by A2,A5,ENUMSET1:39;
then A15: h.A in rng h by FUNCT_1:def 5;
B in dom h by A2,A5,ENUMSET1:39;
then A16: h.B in rng h by FUNCT_1:def 5;
C in dom h by A2,A5,ENUMSET1:39;
then A17: h.C in rng h by FUNCT_1:def 5;
D in dom h by A2,A5,ENUMSET1:39;
then A18: h.D in rng h by FUNCT_1:def 5;
E in dom h by A2,A5,ENUMSET1:39;
then A19: h.E in rng h by FUNCT_1:def 5;
F in dom h by A2,A5,ENUMSET1:39;
then A20: h.F in rng h by FUNCT_1:def 5;
J in dom h by A2,A5,ENUMSET1:39;
then A21: h.J in rng h by FUNCT_1:def 5;
M in dom h by A2,A5,ENUMSET1:39;
then A22: h.M in rng h by FUNCT_1:def 5;
A23:rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M} by Th23;
rng h c= bool Y
proof
let t be set;
assume t in rng h;
then t=h.A or t=h.B or t=h.C or t=h.D or t=h.E or t=h.F or t=h.J
or t=h.M
by A23,ENUMSET1:38;
hence thesis by A6,A7,A8,A9,A10,A11,A12,A13;
end;
then reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
A24: Intersect FF = meet (rng h) by A15,CANTOR_1:def 3;
(Intersect FF)<>{} by A1,A5,A14,BVFUNC_2:def 5;
then consider m being set such that
A25: m in Intersect FF by XBOOLE_0:def 1;
A26: 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)
by A6,A7,A8,A9,A10,A11,A12,A13,A15,A16,A17,A18,A19,A20,A21,A22,A24,A25,
SETFAM_1:def 1;
GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J) /\ EqClass(u,M)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F) /\ EqClass(u,J) /\
EqClass(u,M)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E) /\ EqClass(u,F) /\ EqClass(u
,J) /\
EqClass(u,M)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D) /\ EqClass(u,E) /\ EqClass(u,F) /\
EqClass(u,J) /\ EqClass(u,M)
by BVFUNC14:1;
then GG = ((EqClass(u,B '/\' C) /\ EqClass(u,D)) /\ EqClass(u,E)) /\
EqClass(u,F) /\ EqClass(u,J) /\ EqClass(u,M)
by BVFUNC14:1;
then A27: GG /\ I = ((((EqClass(u,B) /\ EqClass(u,C)) /\ EqClass(u,D)) /\
EqClass(u,E)) /\ EqClass(u,F) /\ EqClass(u,J) /\ EqClass(u,M))
/\
EqClass(z,A) by BVFUNC14:1;
m in EqClass(u,B) /\ EqClass(u,C) by A26,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) by A26,XBOOLE_0:
def 3
;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
by A26,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
/\
EqClass(u,F)
by A26,XBOOLE_0:def 3;
then m in (((EqClass(u,B) /\ EqClass(u,C)) /\ EqClass(u,D)) /\ EqClass(u
,E))
/\
EqClass(u,F) /\ EqClass(u,J)
by A26,XBOOLE_0:def 3;
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 A26,XBOOLE_0:def 3;
then GG /\ I <> {} by A26,A27,XBOOLE_0:def 3;
then consider p being set such that
A28: p in GG /\ I by XBOOLE_0:def 1;
reconsider p as Element of Y by A28;
reconsider K=EqClass(p,C '/\' D '/\' E '/\' F '/\' J '/\' M) as set;
A29:p in K & K in C '/\' D '/\' E '/\' F '/\' J '/\' M by T_1TOPSP:def 1;
p in GG & p in I by A28,XBOOLE_0:def 3;
then A30:p in I /\ K by A29,XBOOLE_0:def 3;
then I /\ K in INTERSECTION(A,C '/\' D '/\' E '/\' F '/\' J '/\' M) &
not (I /\ K in {{}}) by SETFAM_1:def 5,TARSKI:def 1;
then I /\ K in INTERSECTION(A,C '/\' D '/\' E '/\' F '/\' J '/\' M) \ {
{}}
by XBOOLE_0:def 4;
then A31: I /\ K in A '/\' (C '/\' D '/\' E '/\' F '/\' J '/\' M) by PARTIT1:
def 4;
reconsider L=EqClass(z,C '/\' D '/\' E '/\' F '/\' J '/\' M) as set;
GG = EqClass(u,(((B '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J '/\' M)
by PARTIT1:16;
then GG = EqClass(u,((B '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J '/\' M)
by PARTIT1:16;
then GG = EqClass(u,(B '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J '/\' M)
by PARTIT1:16;
then GG = EqClass(u,B '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)
by PARTIT1:16;
then GG = EqClass(u,B '/\' (C '/\' D '/\' E '/\' F '/\' J '/\' M))
by PARTIT1:16;
then A32: GG c= L by A2,BVFUNC11:3;
A33: p in GG by A28,XBOOLE_0:def 3;
p in EqClass(p,C '/\' D '/\' E '/\' F '/\' J '/\' M)
by T_1TOPSP:def 1;
then K meets L by A32,A33,XBOOLE_0:3;
then K=L by T_1TOPSP:9;
then A34:z in K by T_1TOPSP:def 1;
z in I by T_1TOPSP:def 1;
then A35:z in I /\ K by A34,XBOOLE_0:def 3;
z in HH by T_1TOPSP:def 1;
then A36:I /\ K meets HH by A35,XBOOLE_0:3;
A '/\' (C '/\' D '/\' E '/\' F '/\' J '/\' M)
= A '/\' (C '/\' D '/\' E '/\' F '/\' J) '/\' M by PARTIT1:16
.= A '/\' (C '/\' D '/\' E '/\' F) '/\' J '/\' M by PARTIT1:16
.= A '/\' (C '/\' D '/\' E) '/\' F '/\' J '/\' M by PARTIT1:16
.= A '/\' (C '/\' D) '/\' E '/\' F '/\' J '/\' M by PARTIT1:16
.= A '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M by PARTIT1:16;
then p in HH by A3,A30,A31,A36,EQREL_1:def 6;
hence thesis by A4,A33,XBOOLE_0:3;
end;
scheme UI10
{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10()->set,
P[set,set,set,set,set,set,set,set,set,set]}:
P[x1(),x2(),x3(),x4(),x5(),x6(),x7(),x8(),x9(),x10()]
provided
A1: for x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 being set
holds P[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10] by A1;
Lm1: x in union({X,{y}}) iff x in X or x=y
proof
A1: x in union({X,{y}}) implies x in X or x in {y}
proof assume x in union({X,{y}});
then ex Z be set st x in Z & Z in {X,{y}} by TARSKI:def 4;
hence thesis by TARSKI:def 2;
end;
A2: X in {X,{y}} & {y} in {X,{y}} by TARSKI:def 2;
x in {y} iff x=y by TARSKI:def 1;
hence thesis by A1,A2,TARSKI:def 4;
end;
definition
let x1,x2,x3,x4,x5,x6,x7,x8,x9;
func { x1,x2,x3,x4,x5,x6,x7,x8,x9 } -> set means
:Def1: x in it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or
x=x8 or x=x9;
existence
proof
take union({{x1,x2,x3,x4,x5,x6,x7,x8},{x9}});
let x;
x in { x1,x2,x3,x4,x5,x6,x7,x8 } iff
x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x = x6 or
x=x7 or x=x8 by ENUMSET1:38,39;
hence thesis by Lm1;
end;
uniqueness proof
defpred _P[set] means
$1=x1 or $1=x2 or $1=x3 or $1=x4 or $1=x5 or $1=x6 or $1=x7 or $1=x8 or $1=x9;
thus for X, Y being set st
(for x being set holds x in X iff _P[x]) &
(for x being set holds x in Y iff _P[x])
holds X = Y from SetEq;
end;
end;
Lm2:
x in { x1,x2,x3,x4,x5,x6,x7,x8,x9 } iff
x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8 or x=x9
proof
defpred P[set,set,set,set,set,set,set,set,set] means
for X being set holds X = { $1,$2,$3,$4,$5,$6,$7,$8,$9 } iff
for x holds x in
X iff x=$1 or x=$2 or x=$3 or x=$4 or x=$5 or x = $6 or x = $7
or x = $8 or x = $9;
A1: for x1,x2,x3,x4,x5,x6,x7,x8,x9 holds P[x1,x2,x3,x4,x5,x6,x7,x8,x9]
by Def1;
P[x1,x2,x3,x4,x5,x6,x7,x8,x9] from UI9(A1);
hence thesis;
end;
theorem
x in { x1,x2,x3,x4,x5,x6,x7,x8,x9 } implies
x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8
or x=x9 by Lm2;
Lm3: { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
proof
now let x;
A1: x in { x1,x2,x3,x4 } iff x=x1 or x=x2 or x=x3 or x=x4
by ENUMSET1:18,19;
x in { x5,x6,x7,x8,x9 } iff x=x5 or x=x6 or x=x7 or x=x8
or x=x9 by ENUMSET1:23,24;
hence x in { x1,x2,x3,x4,x5,x6,x7,x8,x9 } iff
x in { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 } by A1,Lm2,XBOOLE_0:def 2;
end;
hence thesis by TARSKI:2;
end;
theorem Th27:
{ x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1 } \/ { x2,x3,x4,x5,x6,x7,x8,x9 }
proof
thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 }
= { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 } by Lm3
.= ({ x1 } \/ { x2,x3,x4 }) \/ { x5,x6,x7,x8,x9 } by ENUMSET1:44
.= { x1 } \/ ({ x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }) by XBOOLE_1:4
.= { x1 } \/ { x2,x3,x4,x5,x6,x7,x8,x9 } by ENUMSET1:64;
end;
theorem Th28:
{ x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2 } \/ { x3,x4,x5,x6,x7,x8,x9 }
proof
thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 }
= { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 } by Lm3
.= { x1,x2 } \/ { x3,x4 } \/ { x5,x6,x7,x8,x9 } by ENUMSET1:45
.= { x1,x2 } \/ ({ x3,x4 } \/ { x5,x6,x7,x8,x9 }) by XBOOLE_1:4
.= { x1,x2 } \/ { x3,x4,x5,x6,x7,x8,x9 } by ENUMSET1:57;
end;
theorem Th29:
{ x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3 } \/ { x4,x5,x6,x7,x8,x9 }
proof
thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 }
= { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 } by Lm3
.= { x1,x2,x3 } \/ { x4 } \/ { x5,x6,x7,x8,x9 } by ENUMSET1:46
.= { x1,x2,x3 } \/ ({ x4 } \/ { x5,x6,x7,x8,x9 }) by XBOOLE_1:4
.= { x1,x2,x3 } \/ { x4,x5,x6,x7,x8,x9 } by ENUMSET1:51;
end;
theorem
{ x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 } by Lm3
;
theorem Th31:
{ x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5 } \/ { x6,x7,x8,x9 }
proof
thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 }
= { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 } by Lm3
.= { x1,x2,x3,x4 } \/ ({x5 } \/ { x6,x7,x8,x9 }) by ENUMSET1:47
.= { x1,x2,x3,x4 } \/ {x5 } \/ { x6,x7,x8,x9 } by XBOOLE_1:4
.= { x1,x2,x3,x4,x5 } \/ { x6,x7,x8,x9 } by ENUMSET1:50;
end;
theorem Th32:
{ x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6 } \/ { x7,x8,x9 }
proof
thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 }
= { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 } by Lm3
.= { x1,x2,x3,x4 } \/ ({ x5,x6 } \/ { x7,x8,x9 }) by ENUMSET1:48
.= { x1,x2,x3,x4 } \/ { x5,x6 } \/ { x7,x8,x9 } by XBOOLE_1:4
.= { x1,x2,x3,x4,x5,x6 } \/ { x7,x8,x9 } by ENUMSET1:54;
end;
theorem Th33:
{ x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6,x7 } \/ { x8,x9 }
proof
thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 }
= { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 } by Lm3
.= { x1,x2,x3,x4 } \/ ({ x5,x6,x7 } \/ { x8,x9 }) by ENUMSET1:49
.= { x1,x2,x3,x4 } \/ { x5,x6,x7 } \/ { x8,x9 } by XBOOLE_1:4
.= { x1,x2,x3,x4,x5,x6,x7 } \/ { x8,x9 } by ENUMSET1:59;
end;
theorem
{ x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6,x7,x8 } \/ { x9 }
proof
thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 }
= { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 } by Lm3
.= { x1,x2,x3,x4 } \/ ({ x5,x6,x7,x8 } \/ { x9 }) by ENUMSET1:50
.= { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } \/ { x9 } by XBOOLE_1:4
.= { x1,x2,x3,x4,x5,x6,x7,x8 } \/ { x9 } by ENUMSET1:65;
end;
theorem Th35:
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st 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
holds
CompF(A,G) = B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N
proof
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M,N be a_partition of Y;
assume A1: 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;
A2:CompF(A,G)='/\' (G \ {A}) by BVFUNC_2:def 7;
G \ {A}={A} \/ {B,C,D,E,F,J,M,N} \ {A} by A1,Th27;
then A3:G \ {A} = ({A} \ {A}) \/ ({B,C,D,E,F,J,M,N} \ {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;
A11:not N in {A} by A1,TARSKI:def 1;
A12:{D,E} \ {A} = {D,E} by A6,A7,ZFMISC_1:72;
{B,C,D,E,F,J,M,N} \ {A}
= ({B} \/ {C,D,E,F,J,M,N}) \ {A} by ENUMSET1:62
.= ({B} \ {A}) \/ ({C,D,E,F,J,M,N} \ {A}) by XBOOLE_1:42
.= {B} \/ ({C,D,E,F,J,M,N} \ {A}) by A4,ZFMISC_1:67
.= {B} \/ (({C} \/ {D,E,F,J,M,N}) \ {A}) by ENUMSET1:56
.= {B} \/ (({C} \ {A}) \/ ({D,E,F,J,M,N} \ {A})) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ (({D,E} \/ {F,J,M,N}) \ {A})) by ENUMSET1:52
.= {B} \/ (({C} \ {A}) \/ (({D,E} \ {A}) \/ ({F,J,M,N} \ {A}))) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ ({F,J} \/
{M,N} \ {A}))) by A12,ENUMSET1:45
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ (({F,J} \ {A}) \/ ({M,N} \ {A}))))
by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ ({F,J} \/ ({M,N} \ {A}))))
by A8,A9,ZFMISC_1:72
.= {B} \/ ({C} \/ ({D,E} \/ ({F,J} \/ ({M,N} \ {A})))) by A5,ZFMISC_1:67
.= {B} \/ ({C} \/ ({D,E} \/ ({F,J} \/ {M,N}))) by A10,A11,ZFMISC_1:72
.= {B} \/ ({C} \/ ({D,E} \/ {F,J,M,N})) by ENUMSET1:45
.= {B} \/ ({C} \/ {D,E,F,J,M,N}) by ENUMSET1:52
.= {B} \/ {C,D,E,F,J,M,N} by ENUMSET1:56
.= {B,C,D,E,F,J,M,N} by ENUMSET1:62;
then A13:G \ {A} = {} \/ {B,C,D,E,F,J,M,N} by A3,XBOOLE_1:37;
A14:B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N c= '/\' (G \ {A})
proof
let x be set;
assume A15:x in B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M,N) \ {
{}}
by PARTIT1:def 4;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M,N) &
not x in {{}}
by XBOOLE_0:def 4;
then consider bcdefjm,n being set such that
A16: bcdefjm in B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M &
n in N & x = bcdefjm /\ n by SETFAM_1:def 5;
bcdefjm in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J,M) \ {{}}
by A16,PARTIT1:def 4;
then bcdefjm in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J,M) &
not bcdefjm in {{}} by XBOOLE_0:def 4;
then consider bcdefj,m being set such that
A17: bcdefj in B '/\' C '/\' D '/\' E '/\' F '/\' J & m in M &
bcdefjm = bcdefj /\ m
by SETFAM_1:def 5;
bcdefj in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F,J) \ {{}}
by A17,PARTIT1:def 4;
then bcdefj in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F,J) &
not bcdefj in {{}}
by XBOOLE_0:def 4;
then consider bcdef,j being set such that
A18: 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 A18,PARTIT1:def 4;
then bcdef in INTERSECTION(B '/\' C '/\' D '/\' E,F) & not bcdef in {{}}
by XBOOLE_0:def 4;
then consider bcde,f being set such that
A19: 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 A19,PARTIT1:def 4;
then bcde in INTERSECTION(B '/\' C '/\' D,E) & not bcde in {{}}
by XBOOLE_0:def 4;
then consider bcd,e being set such that
A20: bcd in B '/\' C '/\' D & e in E & bcde = bcd /\ e by SETFAM_1:def 5;
bcd in INTERSECTION(B '/\' C,D) \ {{}} by A20,PARTIT1:def 4;
then bcd in INTERSECTION(B '/\' C,D) & not bcd in {{}} by XBOOLE_0:def 4;
then consider bc,d being set such that
A21: bc in B '/\' C & d in D & bcd = bc /\ d by SETFAM_1:def 5;
bc in INTERSECTION(B,C) \ {{}} by A21,PARTIT1:def 4;
then bc in INTERSECTION(B,C) & not bc in {{}} by XBOOLE_0:def 4;
then consider b,c being set such that
A22: 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) +* (N .--> n);
A23: dom ((B .--> b) +* (C .--> c) +* (D .--> d) +* (E .--> e) +* (F .--> f)
+* (J .--> j) +* (M .--> m) +* (N .--> n))
= {N,B,C,D,E,F,J,M} by Th22
.= {N} \/ {B,C,D,E,F,J,M} by ENUMSET1:62
.= {B,C,D,E,F,J,M,N} by ENUMSET1:68;
A24: h.D = d by A1,Th21;
A25: h.B = b by A1,Th21;
A26: h.C = c by A1,Th21;
A27: h.E = e by A1,Th21;
A28: h.F = f by A1,Th21;
A29: h.J = j by A1,Th21;
A30: h.M = m by A1,BVFUNC14:15;
A31: h.N = n by YELLOW14:3;
A32: for p being set st p in (G \ {A}) holds h.p in p
proof
let p be set;
assume p in (G \ {A});
then p=B or p=C or p=D or p=E or p=F or p=J or p=M or p=N
by A13,ENUMSET1:38;
hence thesis by A1,A16,A17,A18,A19,A20,A21,A22,Th21,BVFUNC14:15,
YELLOW14:3;
end;
A33: D in dom h by A23,ENUMSET1:39;
then A34: h.D in rng h by FUNCT_1:def 5;
A35: B in dom h by A23,ENUMSET1:39;
A36: C in dom h by A23,ENUMSET1:39;
A37: E in dom h by A23,ENUMSET1:39;
A38: F in dom h by A23,ENUMSET1:39;
A39: J in dom h by A23,ENUMSET1:39;
A40: M in dom h by A23,ENUMSET1:39;
A41: N in dom h by A23,ENUMSET1:39;
A42:rng h c= {h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N}
proof
let t be set;
assume t in rng h;
then consider x1 being set such that
A43: x1 in dom h & t = h.x1 by FUNCT_1:def 5;
now per cases by A23,A43,ENUMSET1:38;
case x1=D; hence thesis by A43,ENUMSET1:39;
case x1=B; hence thesis by A43,ENUMSET1:39;
case x1=C; hence thesis by A43,ENUMSET1:39;
case x1=E; hence thesis by A43,ENUMSET1:39;
case x1=F; hence thesis by A43,ENUMSET1:39;
case x1=J; hence thesis by A43,ENUMSET1:39;
case x1=M; hence thesis by A43,ENUMSET1:39;
case x1=N; hence thesis by A43,ENUMSET1:39;
end;
hence thesis;
end;
{h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N} c= rng h
proof
let t be set;
assume A44:t in {h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N};
now per cases by A44,ENUMSET1:38;
case t=h.D; hence thesis by A33,FUNCT_1:def 5;
case t=h.B; hence thesis by A35,FUNCT_1:def 5;
case t=h.C; hence thesis by A36,FUNCT_1:def 5;
case t=h.E; hence thesis by A37,FUNCT_1:def 5;
case t=h.F; hence thesis by A38,FUNCT_1:def 5;
case t=h.J; hence thesis by A39,FUNCT_1:def 5;
case t=h.M; hence thesis by A40,FUNCT_1:def 5;
case t=h.N; hence thesis by A41,FUNCT_1:def 5;
end;
hence thesis;
end;
then A45:rng h = {h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N} by A42,XBOOLE_0:def 10
;
rng h c= bool Y
proof
let t be set;
assume A46:t in rng h;
now per cases by A42,A46,ENUMSET1:38;
case t=h.D; hence thesis by A21,A24;
case t=h.B; hence thesis by A22,A25;
case t=h.C; hence thesis by A22,A26;
case t=h.E; hence thesis by A20,A27;
case t=h.F; hence thesis by A19,A28;
case t=h.J; hence thesis by A18,A29;
case t=h.M; hence thesis by A17,A30;
case t=h.N; hence thesis by A16,A31;
end;
hence thesis;
end;
then reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
reconsider h as Function;
A47: Intersect FF = meet (rng h) by A34,CANTOR_1:def 3;
A48:x c= Intersect FF
proof
let u be set;
assume A49:u in x;
A50:FF<>{} by A45,ENUMSET1:39;
for y be set holds y in FF implies u in y
proof
let y be set;
assume A51: y in FF;
now per cases by A42,A51,ENUMSET1:38;
case A52: y=h.D;
u in (d /\ ((b /\ c) /\ e)) /\ f /\ j /\ m /\
n by A16,A17,A18,A19,A20,A21,A22,A49,XBOOLE_1:16;
then u in (d /\ ((b /\ c) /\ e /\ f)) /\ j /\ m /\ n by XBOOLE_1:16;
then u in d /\ (((b /\ c) /\ e /\ f) /\ j) /\ m /\ n by XBOOLE_1:16;
then u in d /\ ((((b /\ c) /\ e /\ f) /\ j) /\ m) /\ n by XBOOLE_1:16;
then u in d /\ ((((b /\ c) /\ e /\ f) /\ j) /\ m /\ n) by XBOOLE_1:16;
hence thesis by A24,A52,XBOOLE_0:def 3;
case A53: y=h.B;
u in (c /\ (d /\ b)) /\ e /\ f /\ j /\ m /\ n by A16,A17,A18,A19,A20,
A21,A22,A49,XBOOLE_1:16;
then u in c /\ ((d /\ b) /\ e) /\ f /\ j /\ m /\ n by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ b) /\ f /\ j /\ m /\ n by XBOOLE_1:16;
then u in c /\ (((d /\ e) /\ b) /\ f) /\ j /\ m /\ n by XBOOLE_1:16;
then u in c /\ ((((d /\ e) /\ b) /\ f) /\ j) /\ m /\ n by XBOOLE_1:16;
then u in c /\ (((d /\ e) /\ (f /\ b)) /\ j) /\ m /\ n by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ ((f /\ b) /\ j)) /\ m /\ n by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ (f /\ (j /\ b))) /\ m /\ n by XBOOLE_1:16;
then u in (c /\ (d /\ e)) /\ (f /\ (j /\ b)) /\ m /\ n by XBOOLE_1:16;
then u in ((c /\ (d /\ e)) /\ f) /\ (j /\ b) /\ m /\ n by XBOOLE_1:16;
then u in (((c /\ (d /\ e)) /\ f) /\ j) /\ b /\ m /\ n by XBOOLE_1:16;
then u in (((c /\ (d /\ e)) /\ f) /\ j) /\ (m /\ b) /\ n by XBOOLE_1:16
;
then u in (((c /\ (d /\ e)) /\ f) /\ j) /\ (m /\ b /\ n) by XBOOLE_1:16
;
then u in (((c /\ (d /\ e)) /\ f) /\ j) /\ (m /\ (b /\ n)) by XBOOLE_1:
16
;
then u in (((c /\ (d /\ e)) /\ f) /\ j) /\ m /\ (n /\ b) by XBOOLE_1:16
;
then u in (((c /\ (d /\ e)) /\ f) /\ j) /\ m /\ n /\ b by XBOOLE_1:16;
hence thesis by A25,A53,XBOOLE_0:def 3;
case A54: y=h.C;
u in (c /\ (d /\ b)) /\ e /\ f /\ j /\ m /\ n by A16,A17,A18,A19,A20,
A21,A22,A49,XBOOLE_1:16;
then u in c /\ ((d /\ b) /\ e) /\ f /\ j /\ m /\ n by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ b) /\ f /\ j /\ m /\ n by XBOOLE_1:16;
then u in c /\ (((d /\ e) /\ b) /\ f) /\ j /\ m /\ n by XBOOLE_1:16;
then u in c /\ ((((d /\ e) /\ b) /\ f) /\ j) /\ m /\ n by XBOOLE_1:16;
then u in c /\ (((((d /\ e) /\ b) /\ f) /\ j) /\ m) /\ n by XBOOLE_1:16
;
then u in c /\ ((((((d /\ e) /\ b) /\ f) /\ j) /\ m) /\ n) by XBOOLE_1:
16;
hence thesis by A26,A54,XBOOLE_0:def 3;
case A55: y=h.E;
u in ((b /\ c) /\ d) /\ (f /\ e) /\ j /\ m /\
n by A16,A17,A18,A19,A20,A21,A22,A49,XBOOLE_1:16;
then u in ((b /\ c) /\ d) /\ ((f /\ e) /\ j) /\ m /\ n by XBOOLE_1:16;
then u in ((b /\ c) /\ d) /\ ((f /\ j) /\ e) /\ m /\ n by XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ (f /\ j)) /\ e /\ m /\ n by XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ (f /\ j)) /\ (e /\ m) /\ n by XBOOLE_1:16
;
then u in (((b /\ c) /\ d) /\ (f /\ j)) /\ ((m /\ e) /\ n) by XBOOLE_1:
16
;
then u in (((b /\ c) /\ d) /\ (f /\ j)) /\ (m /\ (n /\ e)) by XBOOLE_1:
16
;
then u in (((b /\ c) /\ d) /\ (f /\ j)) /\ m /\ (n /\ e) by XBOOLE_1:16
;
then u in (((b /\ c) /\ d) /\ (f /\ j)) /\ m /\ n /\ e by XBOOLE_1:16;
hence thesis by A27,A55,XBOOLE_0:def 3;
case A56: y=h.F;
u in (((b /\ c) /\ d) /\ e) /\ j /\ f /\ m /\
n by A16,A17,A18,A19,A20,A21,A22,A49,XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ e) /\ j /\ m /\ f /\ n by XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ e) /\ j /\ m /\ n /\ f by XBOOLE_1:16;
hence thesis by A28,A56,XBOOLE_0:def 3;
case A57: y=h.J;
u in (((b /\ c) /\ d) /\ e) /\ f /\ m /\ j /\
n by A16,A17,A18,A19,A20,A21,A22,A49,XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ e) /\ f /\ m /\ n /\ j by XBOOLE_1:16;
hence thesis by A29,A57,XBOOLE_0:def 3;
case A58: y=h.M;
u in (((b /\ c) /\ d) /\ e) /\ f /\ j /\ n /\ m by A16,A17,A18,A19,
A20,A21,A22,A49,XBOOLE_1:16;
hence thesis by A30,A58,XBOOLE_0:def 3;
case y=h.N;
hence thesis by A16,A31,A49,XBOOLE_0:def 3;
end;
hence thesis;
end;
then u in meet FF by A50,SETFAM_1:def 1;
hence thesis by A50,CANTOR_1:def 3;
end;
Intersect FF c= x
proof
let t be set;
assume A59: t in Intersect FF;
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 & h.N in rng h by A45,ENUMSET1:39;
then A60:t in b & t in c & t in d & t in e & t in f & t in j & t in m & t
in n
by A24,A25,A26,A27,A28,A29,A30,A31,A47,A59,SETFAM_1:def 1;
then t in b /\ c by XBOOLE_0:def 3;
then t in (b /\ c) /\ d by A60,XBOOLE_0:def 3;
then t in (b /\ c) /\ d /\ e by A60,XBOOLE_0:def 3;
then t in (b /\ c) /\ d /\ e /\ f by A60,XBOOLE_0:def 3;
then t in (b /\ c) /\ d /\ e /\ f /\ j by A60,XBOOLE_0:def 3;
then t in (b /\ c) /\ d /\ e /\ f /\ j /\ m by A60,XBOOLE_0:def 3;
hence thesis by A16,A17,A18,A19,A20,A21,A22,A60,XBOOLE_0:def 3;
end;
then A61:x = Intersect FF by A48,XBOOLE_0:def 10;
x<>{} by A15,EQREL_1:def 6;
hence thesis by A13,A23,A32,A61,BVFUNC_2:def 1;
end;
'/\' (G \ {A}) c= B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N
proof
let x be set;
assume x in '/\' (G \ {A});
then consider h being Function, FF being Subset-Family of Y such that
A62: 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;
A63: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}) & N in (G \ {A})
by A13,ENUMSET1:39;
then A64: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 & h.N in N by A62;
A65: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 & h.N in rng h
by A62,A63,FUNCT_1:def 5;
then A66:Intersect FF = meet (rng h) by A62,CANTOR_1:def 3;
A67:not (x in {{}}) by A62,TARSKI:def 1;
A68:((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J /\ h.M /\ h.N c= x
proof
let p be set;
assume A69: p in ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J /\ h.M /\
h.N;
then p in ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J /\ h.M & p in h
.
N
by XBOOLE_0:def 3;
then A70: p in ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J & p in h.M
by XBOOLE_0:def 3;
then p in h.B /\ h.C /\ h.D /\ h.E /\ h.F & p in h.J by XBOOLE_0:def 3
;
then A71:p in h.B /\ h.C /\ h.D /\ h.E & p in h.F by XBOOLE_0:def 3;
then p in h.B /\ h.C /\ h.D & p in h.E & p in h.F by XBOOLE_0:def 3;
then p in h.B /\ h.C & p in h.D by XBOOLE_0:def 3;
then A72: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 & p in h.N
by A69,A70,A71,XBOOLE_0:def 3;
A73:rng h c= {h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N}
proof
let u be set;
assume u in rng h;
then consider x1 being set such that
A74: 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 or x1=N
by A13,A62,A74,ENUMSET1:38;
hence thesis by A74,ENUMSET1:39;
end;
for y being set holds y in rng h implies p in y
proof
let y be set;
assume y in rng h;
hence thesis by A72,A73,ENUMSET1:38;
end;
hence thesis by A62,A65,A66,SETFAM_1:def 1;
end;
A75: x c= ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J /\ h.M /\ h.N
proof
let p be set;
assume p in x;
then A76: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 & p in h.N
by A62,A65,A66,SETFAM_1:def 1;
then p in h.B /\ h.C by XBOOLE_0:def 3;
then p in h.B /\ h.C /\ h.D by A76,XBOOLE_0:def 3;
then p in h.B /\ h.C /\ h.D /\ h.E by A76,XBOOLE_0:def 3;
then p in h.B /\ h.C /\ h.D /\ h.E /\ h.F by A76,XBOOLE_0:def 3;
then p in ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\
h.J by A76,XBOOLE_0:def 3;
then p in ((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J /\
h.M by A76,XBOOLE_0:def 3;
hence thesis by A76,XBOOLE_0:def 3;
end;
then A77:((((h.B /\ h.C) /\ h.D) /\ h.E) /\ h.F) /\ h.J /\ h.M /\ h.N = x
by A68,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;
set mbcdefjm=((h.B /\ h.C) /\ h.D) /\ h.E /\ h.F /\ h.J /\ h.M;
mbcdefjm<>{} by A62,A68,A75,XBOOLE_0:def 10;
then A78:not (mbcdefjm in {{}}) by TARSKI:def 1;
mbcdefj<>{} by A62,A68,A75,XBOOLE_0:def 10;
then A79:not (mbcdefj in {{}}) by TARSKI:def 1;
mbcdef<>{} by A62,A68,A75,XBOOLE_0:def 10;
then A80:not (mbcdef in {{}}) by TARSKI:def 1;
mbcde<>{} by A62,A68,A75,XBOOLE_0:def 10;
then A81:not (mbcde in {{}}) by TARSKI:def 1;
mbcd<>{} by A62,A68,A75,XBOOLE_0:def 10;
then A82:not (mbcd in {{}}) by TARSKI:def 1;
mbc<>{} by A62,A68,A75,XBOOLE_0:def 10;
then A83:not (mbc in {{}}) by TARSKI:def 1;
mbc in INTERSECTION(B,C) by A64,SETFAM_1:def 5;
then mbc in INTERSECTION(B,C) \ {{}} by A83,XBOOLE_0:def 4;
then mbc in B '/\' C by PARTIT1:def 4;
then mbcd in INTERSECTION(B '/\' C,D) by A64,SETFAM_1:def 5;
then mbcd in INTERSECTION(B '/\' C,D) \ {{}} by A82,XBOOLE_0:def 4;
then mbcd in B '/\' C '/\' D by PARTIT1:def 4;
then mbcde in INTERSECTION(B '/\' C '/\' D,E) by A64,SETFAM_1:def 5;
then mbcde in INTERSECTION(B '/\' C '/\' D,E) \ {{}} by A81,XBOOLE_0:def 4
;
then mbcde in (B '/\' C '/\' D '/\' E) by PARTIT1:def 4;
then mbcdef in INTERSECTION(B '/\' C '/\' D '/\' E,F) by A64,SETFAM_1:def 5
;
then mbcdef in INTERSECTION(B '/\' C '/\' D '/\' E,F) \ {{}}
by A80,XBOOLE_0:def 4;
then mbcdef in (B '/\' C '/\' D '/\' E '/\' F) by PARTIT1:def 4;
then mbcdefj in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F,J)
by A64,SETFAM_1:def 5;
then mbcdefj in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F,J) \ {{}}
by A79,XBOOLE_0:def 4;
then mbcdefj in (B '/\' C '/\' D '/\' E '/\' F '/\' J) by PARTIT1:def 4;
then mbcdefjm in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J,M)
by A64,SETFAM_1:def 5;
then mbcdefjm in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J,M) \ {
{}}
by A78,XBOOLE_0:def 4;
then mbcdefjm in (B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M)
by PARTIT1:def 4;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M,N)
by A64,A77,SETFAM_1:def 5;
then x in INTERSECTION(B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M,N) \ {
{}}
by A67,XBOOLE_0:def 4;
hence thesis by PARTIT1:def 4;
end;
hence thesis by A2,A14,XBOOLE_0:def 10;
end;
theorem Th36:
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st 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
holds
CompF(B,G) = A '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N
proof
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M,N be a_partition of Y;
{A,B,C,D,E,F,J,M,N} ={A,B} \/ {C,D,E,F,J,M,N} by Th28
.={B,A,C,D,E,F,J,M,N} by Th28;
hence thesis by Th35;
end;
theorem Th37:
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st 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
holds
CompF(C,G) = A '/\' B '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N
proof
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M,N be a_partition of Y;
{A,B,C,D,E,F,J,M,N} ={A,B,C} \/ {D,E,F,J,M,N} by Th29
.={A} \/ {B,C} \/ {D,E,F,J,M,N} by ENUMSET1:42
.={A,C,B} \/ {D,E,F,J,M,N} by ENUMSET1:42
.={A,C,B,D,E,F,J,M,N} by Th29;
hence thesis by Th36;
end;
theorem Th38:
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st 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
holds
CompF(D,G) = A '/\' B '/\' C '/\' E '/\' F '/\' J '/\' M '/\' N
proof
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M,N be a_partition of Y;
{A,B,C,D,E,F,J,M,N} ={A,B} \/ {C,D,E,F,J,M,N} by Th28
.={A,B} \/ ({C,D} \/ {E,F,J,M,N}) by ENUMSET1:57
.={A,B} \/ {D,C,E,F,J,M,N} by ENUMSET1:57
.={A,B,D,C,E,F,J,M,N} by Th28;
hence thesis by Th37;
end;
theorem Th39:
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st 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
holds
CompF(E,G) = A '/\' B '/\' C '/\' D '/\' F '/\' J '/\' M '/\' N
proof
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M,N be a_partition of Y;
{A,B,C,D,E,F,J,M,N} ={A,B,C} \/ {D,E,F,J,M,N} by Th29
.={A,B,C} \/ ({D,E} \/ {F,J,M,N}) by ENUMSET1:52
.={A,B,C} \/ ({E,D,F,J,M,N}) by ENUMSET1:52
.={A,B,C,E,D,F,J,M,N} by Th29;
hence thesis by Th38;
end;
theorem Th40:
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st 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
holds
CompF(F,G) = A '/\' B '/\' C '/\' D '/\' E '/\' J '/\' M '/\' N
proof
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M,N be a_partition of Y;
{A,B,C,D,E,F,J,M,N} ={A,B,C,D} \/ {E,F,J,M,N} by Lm3
.={A,B,C,D} \/ ({E,F} \/ {J,M,N}) by ENUMSET1:48
.={A,B,C,D} \/ ({F,E,J,M,N}) by ENUMSET1:48
.={A,B,C,D,F,E,J,M,N} by Lm3;
hence thesis by Th39;
end;
theorem Th41:
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st 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
holds
CompF(J,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' M '/\' N
proof
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M,N be a_partition of Y;
{A,B,C,D,E,F,J,M,N} ={A,B,C,D,E} \/ {F,J,M,N} by Th31
.={A,B,C,D,E} \/ ({J,F} \/ {M,N}) by ENUMSET1:45
.={A,B,C,D,E} \/ ({J,F,M,N}) by ENUMSET1:45
.={A,B,C,D,E,J,F,M,N} by Th31;
hence thesis by Th40;
end;
theorem Th42:
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st 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
holds
CompF(M,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' N
proof
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M,N be a_partition of Y;
{A,B,C,D,E,F,J,M,N} ={A,B,C,D,E,F} \/ {J,M,N} by Th32
.={A,B,C,D,E,F} \/ ({J,M} \/ {N}) by ENUMSET1:43
.={A,B,C,D,E,F} \/ {M,J,N} by ENUMSET1:43
.={A,B,C,D,E,F,M,J,N} by Th32;
hence thesis by Th41;
end;
theorem
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st 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
holds
CompF(N,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M
proof
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M,N be a_partition of Y;
{A,B,C,D,E,F,J,M,N} ={A,B,C,D,E,F,J} \/ {M,N} by Th33
.={A,B,C,D,E,F,J,N,M} by Th33;
hence thesis by Th42;
end;
theorem Th44:
for A,B,C,D,E,F,J,M,N being set, h being Function,
A',B',C',D',E',F',J',M',N' being set st
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 &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(M .--> M') +* (N .--> N') +* (A .--> A')
holds h.A = A' & h.B = B' & h.C = C' &
h.D = D' & h.E = E' & h.F = F' &
h.J = J' & h.M = M' & h.N = N'
proof
let A,B,C,D,E,F,J,M,N be set;
let h be Function;
let A',B',C',D',E',F',J',M',N' be set;
assume A1:
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 &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(M .--> M') +* (N .--> N') +* (A .--> A');
A2: dom (A .--> A') = {A} by CQC_LANG:5;
A3: h.A = A'
proof
A in dom (A .--> A') by A2,TARSKI:def 1;
then h.A = (A .--> A').A by A1,FUNCT_4:14;
hence thesis by CQC_LANG:6;
end;
A4: h.B = B'
proof
not B in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.B=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M') +* (N .--> N')).B
by A1,FUNCT_4:12
.= B' by A1,Th21;
hence thesis;
end;
A5: h.C = C'
proof
not C in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.C=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M') +* (N .--> N')).C
by A1,FUNCT_4:12;
hence thesis by A1,Th21;
end;
A6: h.D = D'
proof
not D in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.D=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M') +* (N .--> N')).D
by A1,FUNCT_4:12
.= D' by A1,Th21;
hence thesis;
end;
A7: h.E = E'
proof
not E in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.E=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M') +* (N .--> N')).E
by A1,FUNCT_4:12
.= E' by A1,Th21;
hence thesis;
end;
A8: h.F = F'
proof
not F in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.F=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M') +* (N .--> N')).F
by A1,FUNCT_4:12
.= F' by A1,Th21;
hence thesis;
end;
A9: h.J = J'
proof
not J in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.J=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M') +* (N .--> N')).J
by A1,FUNCT_4:12
.= J' by A1,Th21;
hence thesis;
end;
A10: h.M = M'
proof
not M in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.M=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M') +* (N .--> N')).M
by A1,FUNCT_4:12
.= M' by A1,BVFUNC14:15;
hence thesis;
end;
h.N = N'
proof
not N in dom (A .--> A') by A1,A2,TARSKI:def 1;
then h.N=((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M') +* (N .--> N')).N
by A1,FUNCT_4:12
.= N' by YELLOW14:3;
hence thesis;
end;
hence thesis by A3,A4,A5,A6,A7,A8,A9,A10;
end;
theorem Th45:
for A,B,C,D,E,F,J,M,N being set, h being Function,
A',B',C',D',E',F',J',M',N' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(M .--> M') +* (N .--> N') +* (A .--> A')
holds dom h = {A,B,C,D,E,F,J,M,N}
proof
let A,B,C,D,E,F,J,M,N be set;
let h be Function;
let A',B',C',D',E',F',J',M',N' be set;
assume A1:
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(M .--> M') +* (N .--> N') +* (A .--> A');
A2: dom ((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M') +* (N .--> N'))
= {N,B,C,D,E,F,J,M} by Th22
.= {N} \/ {B,C,D,E,F,J,M} by ENUMSET1:62
.= {B,C,D,E,F,J,M,N} by ENUMSET1:68;
dom (A .--> A') = {A} by CQC_LANG:5;
then dom ((B .--> B') +* (C .--> C') +* (D .--> D') +* (E .--> E') +*
(F .--> F') +* (J .--> J') +* (M .--> M') +* (N .--> N') +*(A .--> A'))
= {B,C,D,E,F,J,M,N} \/ {A} by A2,FUNCT_4:def 1
.= {A,B,C,D,E,F,J,M,N} by Th27;
hence thesis by A1;
end;
theorem Th46:
for A,B,C,D,E,F,J,M,N being set, h being Function,
A',B',C',D',E',F',J',M',N' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(M .--> M') +* (N .--> N') +* (A .--> A')
holds rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N}
proof
let A,B,C,D,E,F,J,M,N be set;
let h be Function;
let A',B',C',D',E',F',J',M',N' be set;
assume
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
(E .--> E') +* (F .--> F') +* (J .--> J') +*
(M .--> M') +* (N .--> N') +* (A .--> A');
then A1: dom h = {A,B,C,D,E,F,J,M,N} by Th45;
then A2: A in dom h by Lm2;
A3: B in dom h by A1,Lm2;
A4: C in dom h by A1,Lm2;
A5: D in dom h by A1,Lm2;
A6: E in dom h by A1,Lm2;
A7: F in dom h by A1,Lm2;
A8: J in dom h by A1,Lm2;
A9: M in dom h by A1,Lm2;
A10: N in dom h by A1,Lm2;
A11:rng h c= {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N}
proof
let t be set;
assume t in rng h;
then consider x1 being set such that
A12: x1 in dom h & t = h.x1 by FUNCT_1:def 5;
now per cases by A1,A12,Lm2;
case x1=A; hence thesis by A12,Lm2;
case x1=B; hence thesis by A12,Lm2;
case x1=C; hence thesis by A12,Lm2;
case x1=D; hence thesis by A12,Lm2;
case x1=E; hence thesis by A12,Lm2;
case x1=F; hence thesis by A12,Lm2;
case x1=J; hence thesis by A12,Lm2;
case x1=M; hence thesis by A12,Lm2;
case x1=N; hence thesis by A12,Lm2;
end;
hence thesis;
end;
{h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N} c= rng h
proof
let t be set;
assume A13:t in {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N};
now per cases by A13,Lm2;
case t=h.A; hence thesis by A2,FUNCT_1:def 5;
case t=h.B; hence thesis by A3,FUNCT_1:def 5;
case t=h.C; hence thesis by A4,FUNCT_1:def 5;
case t=h.D; hence thesis by A5,FUNCT_1:def 5;
case t=h.E; hence thesis by A6,FUNCT_1:def 5;
case t=h.F; hence thesis by A7,FUNCT_1:def 5;
case t=h.J; hence thesis by A8,FUNCT_1:def 5;
case t=h.M; hence thesis by A9,FUNCT_1:def 5;
case t=h.N; hence thesis by A10,FUNCT_1:def 5;
end;
hence thesis;
end;
hence thesis by A11,XBOOLE_0:def 10;
end;
theorem
for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
, z,u being Element of Y, h being Function
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
holds EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N) /\
EqClass(z,A) <> {}
proof
let a be Element of Funcs(Y,BOOLEAN);
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M,N be a_partition of Y;
let z,u be Element of Y;
let h be Function;
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;
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));
A3: dom h = G by A2,Th45;
A4: h.A = EqClass(z,A) by A2,Th44;
A5: h.B = EqClass(u,B) by A2,Th44;
A6: h.C = EqClass(u,C) by A2,Th44;
A7: h.D = EqClass(u,D) by A2,Th44;
A8: h.E = EqClass(u,E) by A2,Th44;
A9: h.F = EqClass(u,F) by A2,Th44;
A10: h.J = EqClass(u,J) by A2,Th44;
A11: h.M = EqClass(u,M) by A2,Th44;
A12: h.N = EqClass(u,N) by A2,Th44;
A13: for d being set st d in G holds h.d in d
proof
let d be set;
assume d in G;
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,Lm2;
hence thesis by A4,A5,A6,A7,A8,A9,A10,A11,A12;
end;
A in dom h by A2,A3,Lm2;
then A14: h.A in rng h by FUNCT_1:def 5;
B in dom h by A2,A3,Lm2;
then A15: h.B in rng h by FUNCT_1:def 5;
C in dom h by A2,A3,Lm2;
then A16: h.C in rng h by FUNCT_1:def 5;
D in dom h by A2,A3,Lm2;
then A17: h.D in rng h by FUNCT_1:def 5;
E in dom h by A2,A3,Lm2;
then A18: h.E in rng h by FUNCT_1:def 5;
F in dom h by A2,A3,Lm2;
then A19: h.F in rng h by FUNCT_1:def 5;
J in dom h by A2,A3,Lm2;
then A20: h.J in rng h by FUNCT_1:def 5;
M in dom h by A2,A3,Lm2;
then A21: h.M in rng h by FUNCT_1:def 5;
N in dom h by A2,A3,Lm2;
then A22: h.N in rng h by FUNCT_1:def 5;
A23:rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N} by Th46;
rng h c= bool Y
proof
let t be set;
assume t in rng h;
then t=h.A or t=h.B or t=h.C or t=h.D or t=h.E or t=h.F or
t=h.J or t=h.M or t=h.N
by A23,Lm2;
hence thesis by A4,A5,A6,A7,A8,A9,A10,A11,A12;
end;
then reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
A24: Intersect FF = meet (rng h) by A14,CANTOR_1:def 3;
(Intersect FF)<>{} by A1,A3,A13,BVFUNC_2:def 5;
then consider m being set such that
A25: m in Intersect FF by XBOOLE_0:def 1;
A26: 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 A4,A5,A6,A7,A8,A9,A10,A11,A12,A14,A15,A16,A17,A18,A19,A20,A21,A22,A24,
A25,SETFAM_1:def 1;
GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M) /\
EqClass(u,N) by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J) /\
EqClass(u,M) /\ EqClass(u,N)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F) /\ EqClass(u,J) /\
EqClass(u,M) /\ EqClass(u,N)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E) /\ EqClass(u,F) /\ EqClass(u
,J) /\
EqClass(u,M) /\ EqClass(u,N)
by BVFUNC14:1;
then GG = (EqClass(u,B '/\' C '/\' D) /\ EqClass(u,E)) /\ EqClass(u,F)
/\
EqClass(u,J) /\ EqClass(u,M) /\ EqClass(u,N)
by BVFUNC14:1;
then GG = ((((EqClass(u,B '/\' C) /\ EqClass(u,D)) /\ EqClass(u,E)) /\
EqClass(u,F)) /\ EqClass(u,J)) /\ EqClass(u,M) /\ EqClass(u,N)
by BVFUNC14:1;
then A27: GG /\ EqClass(z,A) = ((((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 BVFUNC14:1;
m in EqClass(u,B) /\ EqClass(u,C) by A26,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) by A26,XBOOLE_0:
def 3
;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
by A26,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
/\
EqClass(u,F)
by A26,XBOOLE_0:def 3;
then m in ((EqClass(u,B) /\ EqClass(u,C)) /\ EqClass(u,D)) /\ EqClass(u,
E)
/\ EqClass(u,F) /\ EqClass(u,J)
by A26,XBOOLE_0:def 3;
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 A26,XBOOLE_0:def 3;
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 A26,XBOOLE_0:def 3;
hence thesis by A26,A27,XBOOLE_0:def 3;
end;
theorem
for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y, 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))
proof
let a be Element of Funcs(Y,BOOLEAN);
let G be Subset of PARTITIONS(Y);
let A,B,C,D,E,F,J,M,N be a_partition of Y;
let z,u be Element of Y;
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);
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 h = G by A2,Th45;
A6: h.A = EqClass(z,A) by A2,Th44;
A7: h.B = EqClass(u,B) by A2,Th44;
A8: h.C = EqClass(u,C) by A2,Th44;
A9: h.D = EqClass(u,D) by A2,Th44;
A10: h.E = EqClass(u,E) by A2,Th44;
A11: h.F = EqClass(u,F) by A2,Th44;
A12: h.J = EqClass(u,J) by A2,Th44;
A13: h.M = EqClass(u,M) by A2,Th44;
A14: h.N = EqClass(u,N) by A2,Th44;
A15: for d being set st d in G holds h.d in d
proof
let d be set;
assume d in G;
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,Lm2;
hence thesis by A6,A7,A8,A9,A10,A11,A12,A13,A14;
end;
A in dom h by A2,A5,Lm2;
then A16: h.A in rng h by FUNCT_1:def 5;
B in dom h by A2,A5,Lm2;
then A17: h.B in rng h by FUNCT_1:def 5;
C in dom h by A2,A5,Lm2;
then A18: h.C in rng h by FUNCT_1:def 5;
D in dom h by A2,A5,Lm2;
then A19: h.D in rng h by FUNCT_1:def 5;
E in dom h by A2,A5,Lm2;
then A20: h.E in rng h by FUNCT_1:def 5;
F in dom h by A2,A5,Lm2;
then A21: h.F in rng h by FUNCT_1:def 5;
J in dom h by A2,A5,Lm2;
then A22: h.J in rng h by FUNCT_1:def 5;
M in dom h by A2,A5,Lm2;
then A23: h.M in rng h by FUNCT_1:def 5;
N in dom h by A2,A5,Lm2;
then A24: h.N in rng h by FUNCT_1:def 5;
A25:rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N} by Th46;
rng h c= bool Y
proof
let t be set;
assume t in rng h;
then t=h.A or t=h.B or t=h.C or t=h.D or t=h.E or t=h.F or t=h.J
or t=h.M or t=h.N
by A25,Lm2;
hence thesis by A6,A7,A8,A9,A10,A11,A12,A13,A14;
end;
then reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
A26: Intersect FF = meet (rng h) by A16,CANTOR_1:def 3;
(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
;
GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M) /\
EqClass(u,N)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J) /\ EqClass(u,M
)
/\ EqClass(u,N)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E '/\' F) /\ EqClass(u,J) /\
EqClass(u,M) /\ EqClass(u,N)
by BVFUNC14:1;
then GG = EqClass(u,B '/\' C '/\' D '/\' E) /\ EqClass(u,F) /\ EqClass(u
,J) /\
EqClass(u,M) /\ EqClass(u,N)
by BVFUNC14:1;
then GG = (((EqClass(u,B '/\' C '/\' D)) /\ EqClass(u,E)) /\ EqClass(u,F
)) /\
EqClass(u,J) /\ EqClass(u,M) /\ EqClass(u,N)
by BVFUNC14:1;
then GG = ((EqClass(u,B '/\' C) /\ EqClass(u,D)) /\ EqClass(u,E)) /\
EqClass(u,F) /\ EqClass(u,J) /\ EqClass(u,M) /\ EqClass(u,N)
by BVFUNC14:1;
then A29: GG /\ 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 BVFUNC14:1;
m in EqClass(u,B) /\ EqClass(u,C) by A28,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) by A28,XBOOLE_0:
def 3
;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
by A28,XBOOLE_0:def 3;
then m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(u,E)
/\
EqClass(u,F) by A28,XBOOLE_0:def 3;
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 3;
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 3;
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 3;
then A30:GG /\ I <> {} by A28,A29,XBOOLE_0:def 3;
then consider p being set such that
A31: p in GG /\ I by XBOOLE_0:def 1;
GG /\ I in
INTERSECTION(A,B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N) &
not (GG /\ I in {{}}) by A30,SETFAM_1:def 5,TARSKI:def 1;
then GG /\ I in
INTERSECTION(A,B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N)
\ {{}} by XBOOLE_0:def 4;
then GG /\ I in
(A '/\' (((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))
by PARTIT1:def 4;
then reconsider p as Element of Y by A31;
set K=EqClass(p,C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N);
A32:p in K & K in C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N
by T_1TOPSP:def 1;
p in GG & p in I by A31,XBOOLE_0:def 3;
then A33:p in I /\ K by A32,XBOOLE_0:def 3;
then I /\ K in INTERSECTION(A,C '/\' D '/\' E '/\' F '/\' J '/\' M '/\'
N) &
not (I /\ K in {{}})
by SETFAM_1:def 5,TARSKI:def 1;
then A34: I /\ K in INTERSECTION(A,C '/\' D '/\'
E '/\' F '/\' J '/\' M '/\' N) \ {{}}
by XBOOLE_0:def 4;
set L=EqClass(z,C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N);
GG=EqClass(u,(((B '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J '/\' M '/\' N
)
by PARTIT1:16;
then GG=EqClass(u,((B '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J '/\' M
'/\' N)
by PARTIT1:16;
then GG=EqClass(u,(B '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J '/\' M
'/\' N)
by PARTIT1:16;
then GG=EqClass(u,B '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
'/\' N)
by PARTIT1:16;
then GG=
EqClass(u,B '/\' (((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)
by PARTIT1:16;
then GG=EqClass(u,B '/\' (C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N))
by PARTIT1:16;
then A35: GG c= L by A2,BVFUNC11:3;
A36: p in GG by A31,XBOOLE_0:def 3;
p in EqClass(p,C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N)
by T_1TOPSP:def 1;
then K meets L by A35,A36,XBOOLE_0:3;
then K=L by T_1TOPSP:9;
then A37:z in K by T_1TOPSP:def 1;
z in I by T_1TOPSP:def 1;
then A38:z in I /\ K by A37,XBOOLE_0:def 3;
z in HH by T_1TOPSP:def 1;
then A39:I /\ K meets HH by A38,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 /\ K in CompF(B,G) by A4,A34,PARTIT1:def 4;
then p in HH by A33,A39,EQREL_1:def 6;
hence thesis by A3,A36,XBOOLE_0:3;
end;
theorem
x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8 or x=x9
implies x in { x1,x2,x3,x4,x5,x6,x7,x8,x9 } by Lm2;