Copyright (c) 1990 Association of Mizar Users
environ
vocabulary BOOLE, TARSKI, MCART_1, MCART_2, MCART_3, MCART_4, MCART_5,
MCART_6;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, MCART_2, MCART_3,
MCART_4, MCART_5;
constructors TARSKI, MCART_1, MCART_2, MCART_3, MCART_4, MCART_5, MEMBERED,
XBOOLE_0;
clusters MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;
theorems TARSKI, ZFMISC_1, MCART_1, MCART_2, MCART_3, MCART_4, MCART_5,
XBOOLE_0, XBOOLE_1;
schemes XBOOLE_0;
begin
reserve x1,x2,x3,x4,x5,x6,x7,x8,x9 for set;
reserve y,y1,y2,y3,y4,y5,y6,y7,y8,y9 for set;
reserve X,X1,X2,X3,X4,X5,X6,X7,X8,X9 for set;
reserve Y,Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD,YE,YF for set;
reserve Z,Z1,Z2,Z3,Z4,Z5,Z6,Z7,Z8,Z9,ZA,ZB,ZC,ZD,ZE,ZF for set;
reserve xx1 for Element of X1;
reserve xx2 for Element of X2;
reserve xx3 for Element of X3;
reserve xx4 for Element of X4;
reserve xx5 for Element of X5;
reserve xx6 for Element of X6;
reserve xx7 for Element of X7;
reserve xx8 for Element of X8;
theorem
X <> {} implies
ex Y st Y in X &
for Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD,YE
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in YE & YE
in Y
holds Y1 misses X
proof
defpred P1[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD
& YD in $1 & Y1 meets X;
consider Z1 such that
A1: for Y holds Y in Z1 iff Y in union X & P1[Y] from Separation;
defpred P2[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in $1
& Y1 meets X;
consider Z2 such that
A2: for Y holds Y in Z2 iff Y in union union X & P2[Y] from Separation;
defpred P3[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in $1 & Y1 meets X;
consider Z3 such that
A3: for Y holds Y in Z3 iff Y in union union union X & P3[Y] from Separation;
defpred P4[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in $1 & Y1 meets X;
consider Z4 such that
A4: for Y holds Y in Z4 iff Y in union union union union X & P4[Y]
from Separation;
defpred P5[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in Y9 & Y9 in $1 & Y1 meets X;
consider Z5 such that
A5: for Y holds Y in Z5 iff
Y in union union union union union X & P5[Y] from Separation;
defpred P6[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in $1 & Y1 meets X;
consider Z6 such that
A6: for Y holds Y in Z6 iff
Y in union union union union union union X & P6[Y] from Separation;
defpred P7[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in $1 & Y1 meets X;
consider Z7 such that
A7: for Y holds Y in Z7 iff
Y in union union union union union union union X & P7[Y]
from Separation;
defpred P8[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in $1
& Y1 meets X;
consider Z8 such that
A8: for Y holds Y in Z8 iff
Y in union union union union union union union union X & P8[Y]
from Separation;
defpred P9[set] means
ex Y1,Y2,Y3,Y4,Y5
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in $1 & Y1 meets X;
consider Z9 such that
A9: for Y holds Y in Z9 iff
Y in union union union union union union union union union X & P9[Y]
from Separation;
defpred P10[set] means
ex Y1,Y2,Y3,Y4
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in $1 & Y1 meets X;
consider ZA such that
A10: for Y holds Y in ZA iff
Y in union union union union union union union union union union X &
P10[Y] from Separation;
defpred P11[set] means
ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X;
consider ZB such that
A11: for Y holds Y in ZB iff
Y in union union union union union union union union union union
(union X) & P11[Y] from Separation;
defpred P12[set] means ex Y1,Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X;
consider ZC such that
A12: for Y holds Y in ZC iff
Y in union union union union union union union union union union
(union union X) & P12[Y] from Separation;
defpred P13[set] means ex Y1 st Y1 in $1 & Y1 meets X;
consider ZD such that
A13: for Y holds Y in ZD iff
Y in union union union union union union union union union union
(union union union X) & P13[Y] from Separation;
defpred P14[set] means $1 meets X;
consider ZE such that
A14: for Y holds Y in ZE iff
Y in union union union union union union union union union union
(union union union union X) & P14[Y] from Separation;
set V = (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD
\/ ZE;
A15: V = (X \/ (Z1 \/ Z2) \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/
ZB \/ ZC \/ ZD
\/ ZE by XBOOLE_1:4
.= (X \/ (Z1 \/ Z2 \/ Z3) \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD
\/ ZE by XBOOLE_1:4
.= (X \/ (Z1 \/ Z2 \/ Z3 \/ Z4)) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD
\/ ZE by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/
ZC \/ ZD
\/ ZE by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/
ZC \/ ZD
\/ ZE by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7) \/ Z8 \/ Z9 \/ ZA \/ ZB \/
ZC \/ ZD
\/ ZE by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8) \/ Z9 \/ ZA \/ ZB \/
ZC \/ ZD
\/ ZE by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9) \/ ZA \/ ZB \/
ZC \/ ZD
\/ ZE by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA) \/ ZB \/
ZC \/ ZD
\/ ZE by XBOOLE_1:4
.= X \/ ((Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB)
\/ ZC \/ ZD
\/ ZE by XBOOLE_1:4
.= X \/ ((Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC) \/ ZD
\/ ZE by XBOOLE_1:4
.= X \/ ((Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD)
\/ ZE by XBOOLE_1:4
.= X \/ ((Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD
\/ ZE) by XBOOLE_1:4;
assume X <> {};
then V <> {} by A15,XBOOLE_1:15;
then consider Y such that
A16: Y in V and
A17: Y misses V by MCART_1:1;
assume
A18: not thesis;
Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/
ZB
\/ ZC \/ ZD
or Y in ZE by A16,XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA
\/ ZB \/ ZC
or Y in ZD or Y in ZE by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA
\/ ZB
or Y in ZC or Y in ZD or Y in ZE by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA
or Y in ZB or Y in ZC or Y in ZD or Y in ZE by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 or Y in ZA
or Y in ZB or Y in ZC or Y in ZD or Y in ZE by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 or Y in Z9 or Y in
ZA
or Y in ZB or Y in ZC or Y in ZD or Y in ZE by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/
Z7 or Y in Z8 or Y in Z9
or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in
ZE by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/
Z6 or Y in Z7 or Y in Z8 or Y in
Z9
or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in
ZE by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/
Z5 or Y in Z6 or Y in Z7 or Y in Z8
or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE
by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/
Z4 or Y in Z5 or Y in Z6 or Y in Z7 or Y in
Z8
or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE
by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/
Z3) or Y in Z4 or Y in Z5 or Y in Z6 or Y in Z7
or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in
ZE
by XBOOLE_0:def 2;
then Y in (X \/ Z1) \/
Z2 or Y in Z3 or Y in Z4 or Y in Z5 or Y in Z6 or Y in
Z7
or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in
ZE
by XBOOLE_0:def 2;
then A19: Y in X \/
Z1 or Y in Z2 or Y in Z3 or Y in Z4 or Y in Z5 or Y in Z6 or Y in
Z7
or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in
ZE
by XBOOLE_0:def 2;
per cases by A19,XBOOLE_0:def 2;
suppose
A20: Y in X;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD,YE such that
A21: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in YE & YE in
Y
& not Y1 misses X by A18;
YE in union X & Y1 meets X by A20,A21,TARSKI:def 4;
then YE in Z1 by A1,A21;
then YE in X \/ Z1 by XBOOLE_0:def 2;
then YE in X \/ Z1 \/ Z2 by XBOOLE_0:def 2;
then YE in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2;
then YE in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
then YE in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by A21,XBOOLE_0:3;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA
by XBOOLE_1:70;
then Y meets (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_1:70;
then Y meets (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC by XBOOLE_1:70;
then Y meets (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD by XBOOLE_1:70;
hence contradiction by A17,XBOOLE_1:70;
suppose
A22: Y in Z1;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD such that
A23: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in Y
& Y1 meets X by A1;
Y in union X by A1,A22;
then YD in union union X by A23,TARSKI:def 4;
then YD in Z2 by A2,A23;
then YD in X \/ Z1 \/ Z2 by XBOOLE_0:def 2;
then Y meets X \/ Z1 \/ Z2 by A23,XBOOLE_0:3;
then Y meets X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA
by XBOOLE_1:70;
then Y meets (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_1:70;
then Y meets (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC by XBOOLE_1:70;
then Y meets (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD by XBOOLE_1:70;
hence contradiction by A17,XBOOLE_1:70;
suppose
A24: Y in Z2;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC such that
A25: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in Y & Y1 meets X by A2;
Y in union union X by A2,A24;
then YC in union union union X by A25,TARSKI:def 4;
then YC in Z3 by A3,A25;
then YC in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then YC in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then YC in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then YC in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then YC in V by XBOOLE_0:def 2;
hence contradiction by A17,A25,XBOOLE_0:3;
suppose
A26: Y in Z3;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB such that
A27: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in Y & Y1 meets X by A3;
Y in union union union X by A3,A26;
then YB in union union union union X by A27,TARSKI:def 4;
then YB in Z4 by A4,A27;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then YB in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then YB in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then YB in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then YB in V by XBOOLE_0:def 2;
hence contradiction by A17,A27,XBOOLE_0:3;
suppose
A28: Y in Z4;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA such that
A29: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in Y & Y1 meets X by A4;
Y in union union union union X by A4,A28;
then YA in union union union union union X by A29,TARSKI:def 4;
then YA in Z5 by A5,A29;
then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2;
then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then YA in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then YA in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then YA in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then YA in V by XBOOLE_0:def 2;
hence contradiction by A17,A29,XBOOLE_0:3;
suppose
A30: Y in Z5;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9 such that
A31: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in Y & Y1 meets X by A5;
Y in union union union union union X by A5,A30;
then Y9 in union union union union union union X by A31,TARSKI:def 4;
then Y9 in Z6 by A6,A31;
then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2;
then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then Y9 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then Y9 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then Y9 in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then Y9 in V by XBOOLE_0:def 2;
hence contradiction by A17,A31,XBOOLE_0:3;
suppose
A32: Y in Z6;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8 such that
A33: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y & Y1 meets X by A6;
Y in union union union union union union X by A6,A32;
then Y8 in
union union union union union union union X by A33,TARSKI:def 4;
then Y8 in Z7 by A7,A33;
then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2;
then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then Y8 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then Y8 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then Y8 in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then Y8 in V by XBOOLE_0:def 2;
hence contradiction by A17,A33,XBOOLE_0:3;
suppose
A34: Y in Z7;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7 such that
A35: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y
& Y1 meets X by A7;
Y in union union union union union union union X by A7,A34;
then Y7 in union union union union union union union union X
by A35,TARSKI:def 4;
then Y7 in Z8 by A8,A35;
then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then Y7 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then Y7 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then Y7 in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then Y7 in V by XBOOLE_0:def 2;
hence contradiction by A17,A35,XBOOLE_0:3;
suppose
A36: Y in Z8;
then consider Y1,Y2,Y3,Y4,Y5,Y6 such that
A37: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y
& Y1 meets X by A8;
Y in union union union union union union union union X by A8,A36;
then Y6 in union union union union union union union union union X
by A37,TARSKI:def 4;
then Y6 in Z9 by A9,A37;
then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then Y6 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then Y6 in ((X \/ Z1) \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC by XBOOLE_0:def 2;
then Y6 in ((X \/ Z1) \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD by XBOOLE_0:def 2;
then Y6 in V by XBOOLE_0:def 2;
hence contradiction by A17,A37,XBOOLE_0:3;
suppose
A38: Y in Z9;
then consider Y1,Y2,Y3,Y4,Y5 such that
A39: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y & Y1 meets X by A9;
Y in union union union union union union union union union X by A9,A38;
then Y5 in union union union union union union union union union union X
by A39,TARSKI:def 4;
then Y5 in ZA by A10,A39;
then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then Y5 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then Y5 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then Y5 in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then Y5 in V by XBOOLE_0:def 2;
hence contradiction by A17,A39,XBOOLE_0:3;
suppose
A40: Y in ZA;
then consider Y1,Y2,Y3,Y4 such that
A41: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & Y1 meets X by A10;
Y in union union union union union union union union union union X
by A10,A40;
then Y4 in union union union union union union union union union union
(union X)
by A41,TARSKI:def 4;
then Y4 in ZB by A11,A41;
then Y4 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then Y4 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then Y4 in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then Y4 in V by XBOOLE_0:def 2;
hence contradiction by A17,A41,XBOOLE_0:3;
suppose
A42: Y in ZB;
then consider Y1,Y2,Y3 such that
A43: Y1 in Y2 & Y2 in Y3 & Y3 in Y & Y1 meets X by A11;
Y in union union union union union union union union union union (union
X
)
by A11,A42;
then Y3 in union union union union union union union union union union
(union union X)
by A43,TARSKI:def 4;
then Y3 in ZC by A12,A43;
then Y3 in ((X \/ Z1) \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC by XBOOLE_0:def 2;
then Y3 in ((X \/ Z1) \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD by XBOOLE_0:def 2;
then Y3 in V by XBOOLE_0:def 2;
hence contradiction by A17,A43,XBOOLE_0:3;
suppose
A44: Y in ZC;
then consider Y1,Y2 such that
A45: Y1 in Y2 & Y2 in Y & Y1 meets X by A12;
Y in union union union union union union union union union union
(union union X) by A12,A44;
then Y2 in union union union union union union union union union union
(union union union X)
by A45,TARSKI:def 4;
then Y2 in ZD by A13,A45;
then Y2 in ((X \/ Z1) \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD by XBOOLE_0:def 2;
then Y2 in V by XBOOLE_0:def 2;
hence contradiction by A17,A45,XBOOLE_0:3;
suppose
A46: Y in ZD;
then consider Y1 such that
A47: Y1 in Y & Y1 meets X by A13;
Y in union union union union union union union union union union
(union union union X) by A13,A46;
then Y1 in union union union union union union union union union union
(union union union union X) by A47,TARSKI:def 4;
then Y1 in ZE by A14,A47;
then Y1 in V by XBOOLE_0:def 2;
hence contradiction by A17,A47,XBOOLE_0:3;
suppose Y in ZE;
then Y meets X by A14;
hence contradiction by A15,A17,XBOOLE_1:70;
end;
theorem
X <> {} implies
ex Y st Y in X &
for Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD,YE,YF
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in YE & YE
in YF
& YF in Y
holds Y1 misses X
proof
defpred P1[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD,YE
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD
& YD in YE & YE in $1 & Y1 meets X;
consider Z1 such that
A1: for Y holds Y in Z1 iff Y in union X & P1[Y] from Separation;
defpred P2[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD
& YD in $1 & Y1 meets X;
consider Z2 such that
A2: for Y holds Y in Z2 iff Y in union union X & P2[Y] from Separation;
defpred P3[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in $1
& Y1 meets X;
consider Z3 such that
A3: for Y holds Y in Z3 iff Y in union union union X & P3[Y] from Separation;
defpred P4[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in $1
& Y1 meets X;
consider Z4 such that
A4: for Y holds Y in Z4 iff Y in union union union union X & P4[Y]
from Separation;
defpred P5[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in $1 & Y1 meets X;
consider Z5 such that
A5: for Y holds Y in Z5 iff
Y in union union union union union X & P5[Y]
from Separation;
defpred P6[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in Y9 & Y9 in $1 & Y1 meets X;
consider Z6 such that
A6: for Y holds Y in Z6 iff
Y in union union union union union union X & P6[Y]
from Separation;
defpred P7[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in Y8 & Y8 in $1 & Y1 meets X;
consider Z7 such that
A7: for Y holds Y in Z7 iff
Y in union union union union union union union X & P7[Y]
from Separation;
defpred P8[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6,Y7
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7
& Y7 in $1 & Y1 meets X;
consider Z8 such that
A8: for Y holds Y in Z8 iff
Y in union union union union union union union union X & P8[Y]
from Separation;
defpred P9[set] means
ex Y1,Y2,Y3,Y4,Y5,Y6
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in $1
& Y1 meets X;
consider Z9 such that
A9: for Y holds Y in Z9 iff
Y in union union union union union union union union union X & P9[Y]
from Separation;
defpred P10[set] means
ex Y1,Y2,Y3,Y4,Y5
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in $1
& Y1 meets X;
consider ZA such that
A10: for Y holds Y in ZA iff
Y in union union union union union union union union union union X &
P10[Y] from Separation;
defpred P11[set] means
ex Y1,Y2,Y3,Y4
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in $1 & Y1 meets X;
consider ZB such that
A11: for Y holds Y in ZB iff
Y in union union union union union union union union union union
(union X) & P11[Y] from Separation;
defpred P12[set] means
ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X;
consider ZC such that
A12: for Y holds Y in ZC iff
Y in union union union union union union union union union union
(union union X) & P12[Y] from Separation;
defpred P13[set] means ex Y1,Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X;
consider ZD such that
A13: for Y holds Y in ZD iff
Y in union union union union union union union union union union
(union union union X) & P13[Y] from Separation;
defpred P14[set] means ex Y1 st Y1 in $1 & Y1 meets X;
consider ZE such that
A14: for Y holds Y in ZE iff
Y in union union union union union union union union union union
(union union union union X) & P14[Y] from Separation;
defpred P15[set] means $1 meets X;
consider ZF such that
A15: for Y holds Y in ZF iff
Y in union union union union union union union union union union
(union union union union union X) & P15[Y] from Separation;
set V = (X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD
\/ ZE \/ ZF;
A16: V = (X \/ (Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/
ZB \/ ZC \/ ZD
\/ ZE \/ ZF by XBOOLE_1:4
.= (X \/ (Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5) \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD
\/ ZE \/ ZF by XBOOLE_1:4
.= (X \/ (Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5) \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD
\/ ZE \/ ZF by XBOOLE_1:4
.= (X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5)) \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD
\/ ZE \/ ZF by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/
ZC \/ ZD
\/ ZE \/ ZF by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7) \/ Z8 \/ Z9 \/ ZA \/ ZB \/
ZC \/ ZD
\/ ZE \/ ZF by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8) \/ Z9 \/ ZA \/ ZB \/
ZC \/ ZD
\/ ZE \/ ZF by XBOOLE_1:4
.= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9) \/ ZA \/ ZB \/
ZC \/ ZD
\/ ZE \/ ZF by XBOOLE_1:4
.= X \/ ((Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA) \/ ZB
\/ ZC \/ ZD
\/ ZE \/ ZF by XBOOLE_1:4
.= X \/ ((Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB)
\/ ZC \/ ZD
\/ ZE \/ ZF by XBOOLE_1:4
.= X \/ ((Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC) \/ ZD
\/ ZE \/ ZF by XBOOLE_1:4
.= X \/ ((Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD)
\/ ZE \/ ZF by XBOOLE_1:4
.= X \/ ((Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD
\/ ZE) \/ ZF by XBOOLE_1:4
.= X \/ ((Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB
\/ ZC \/ ZD
\/ ZE \/ ZF) by XBOOLE_1:4;
assume X <> {};
then V <> {} by A16,XBOOLE_1:15;
then consider Y such that
A17: Y in V and
A18: Y misses V by MCART_1:1;
assume
A19: not thesis;
Y in (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/
Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC \/ ZD \/
ZE or Y in ZF by A17,XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA
\/
ZB \/ ZC \/ ZD
or Y in ZE or Y in ZF by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA
\/ ZB \/ ZC
or Y in ZD or Y in ZE or Y in ZF by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA
\/ ZB
or Y in ZC or Y in ZD or Y in ZE or Y in ZF by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA
or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in
ZF by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 or Y in ZA
or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in
ZF by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 or Y in Z9 or Y in
ZA
or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in
ZF by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/
Z7 or Y in Z8 or Y in Z9
or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF
by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/
Z6 or Y in Z7 or Y in Z8 or Y in
Z9
or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF
by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/
Z5 or Y in Z6 or Y in Z7 or Y in Z8
or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y
in ZF
by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/ Z3) \/
Z4 or Y in Z5 or Y in Z6 or Y in Z7 or Y in
Z8
or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y
in ZF
by XBOOLE_0:def 2;
then Y in (X \/ Z1 \/ Z2 \/
Z3) or Y in Z4 or Y in Z5 or Y in Z6 or Y in Z7
or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y
in ZE
or Y in ZF by XBOOLE_0:def 2;
then Y in (X \/ Z1) \/
Z2 or Y in Z3 or Y in Z4 or Y in Z5 or Y in Z6 or Y in
Z7
or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in
ZE
or Y in ZF by XBOOLE_0:def 2;
then A20: Y in X \/
Z1 or Y in Z2 or Y in Z3 or Y in Z4 or Y in Z5 or Y in Z6 or Y in
Z7
or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in
ZE
or Y in ZF by XBOOLE_0:def 2;
per cases by A20,XBOOLE_0:def 2;
suppose
A21: Y in X;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD,YE,YF such that
A22: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in YE & YE in
YF
& YF in Y & not Y1 misses X by A19;
YF in union X & Y1 meets X by A21,A22,TARSKI:def 4;
then YF in Z1 by A1,A22;
then YF in X \/ Z1 by XBOOLE_0:def 2;
then YF in X \/ Z1 \/ Z2 by XBOOLE_0:def 2;
then YF in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2;
then YF in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
then YF in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by A22,XBOOLE_0:3;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA
by XBOOLE_1:70;
then Y meets (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_1:70;
then Y meets (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC by XBOOLE_1:70;
then Y meets (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD by XBOOLE_1:70;
then Y meets (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD \/ ZE by XBOOLE_1:70;
hence contradiction by A18,XBOOLE_1:70;
suppose
A23: Y in Z1;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD,YE such that
A24: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in YE & YE in
Y
& Y1 meets X by A1;
Y in union X by A1,A23;
then YE in union union X by A24,TARSKI:def 4;
then YE in Z2 by A2,A24;
then YE in X \/ Z1 \/ Z2 by XBOOLE_0:def 2;
then Y meets X \/ Z1 \/ Z2 by A24,XBOOLE_0:3;
then Y meets X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_1:70;
then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA
by XBOOLE_1:70;
then Y meets (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_1:70;
then Y meets (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC by XBOOLE_1:70;
then Y meets (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD by XBOOLE_1:70;
then Y meets (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD \/ ZE by XBOOLE_1:70;
hence contradiction by A18,XBOOLE_1:70;
suppose
A25: Y in Z2;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD such that
A26: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in Y
& Y1 meets X by A2;
Y in union union X by A2,A25;
then YD in union union union X by A26,TARSKI:def 4;
then YD in Z3 by A3,A26;
then YD in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2;
then YD in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
then YD in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
then YD in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
then YD in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2;
then YD in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then YD in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then YD in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then YD in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then YD in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then YD in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then YD in (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD \/ ZE by XBOOLE_0:def 2;
then YD in V by XBOOLE_0:def 2;
hence contradiction by A18,A26,XBOOLE_0:3;
suppose
A27: Y in Z3;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC such that
A28: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in Y & Y1 meets X by A3;
Y in union union union X by A3,A27;
then YC in union union union union X by A28,TARSKI:def 4;
then YC in Z4 by A4,A28;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then YC in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then YC in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then YC in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then YC in (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD \/ ZE by XBOOLE_0:def 2;
then YC in V by XBOOLE_0:def 2;
hence contradiction by A18,A28,XBOOLE_0:3;
suppose
A29: Y in Z4;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB such that
A30: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in Y & Y1 meets X by A4;
Y in union union union union X by A4,A29;
then YB in union union union union union X by A30,TARSKI:def 4;
then YB in Z5 by A5,A30;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then YB in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then YB in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then YB in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then YB in (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD \/ ZE by XBOOLE_0:def 2;
then YB in V by XBOOLE_0:def 2;
hence contradiction by A18,A30,XBOOLE_0:3;
suppose
A31: Y in Z5;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA such that
A32: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in Y & Y1 meets X by A5;
Y in union union union union union X by A5,A31;
then YA in union union union union union union X by A32,TARSKI:def 4;
then YA in Z6 by A6,A32;
then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2;
then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2;
then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then YA in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then YA in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then YA in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then YA in (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD \/ ZE by XBOOLE_0:def 2;
then YA in V by XBOOLE_0:def 2;
hence contradiction by A18,A32,XBOOLE_0:3;
suppose
A33: Y in Z6;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9 such that
A34: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in Y & Y1 meets X by A6;
Y in union union union union union union X by A6,A33;
then Y9 in
union union union union union union union X by A34,TARSKI:def 4;
then Y9 in Z7 by A7,A34;
then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2;
then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then Y9 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then Y9 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then Y9 in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then Y9 in (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD \/ ZE by XBOOLE_0:def 2;
then Y9 in V by XBOOLE_0:def 2;
hence contradiction by A18,A34,XBOOLE_0:3;
suppose
A35: Y in Z7;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8 such that
A36: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y & Y1 meets X by A7;
Y in union union union union union union union X by A7,A35;
then Y8 in union union union union union union union union X
by A36,TARSKI:def 4;
then Y8 in Z8 by A8,A36;
then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/
Z8 by XBOOLE_0:def 2;
then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then Y8 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then Y8 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then Y8 in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then Y8 in (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD \/ ZE by XBOOLE_0:def 2;
then Y8 in V by XBOOLE_0:def 2;
hence contradiction by A18,A36,XBOOLE_0:3;
suppose
A37: Y in Z8;
then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7 such that
A38: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y
& Y1 meets X by A8;
Y in union union union union union union union union X by A8,A37;
then Y7 in union union union union union union union union union X
by A38,TARSKI:def 4;
then Y7 in Z9 by A9,A38;
then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/
Z9 by XBOOLE_0:def 2;
then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then Y7 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then Y7 in ((X \/ Z1) \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC by XBOOLE_0:def 2;
then Y7 in ((X \/ Z1) \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD by XBOOLE_0:def 2;
then Y7 in ((X \/ Z1) \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD \/ ZE by XBOOLE_0:def 2;
then Y7 in V by XBOOLE_0:def 2;
hence contradiction by A18,A38,XBOOLE_0:3;
suppose
A39: Y in Z9;
then consider Y1,Y2,Y3,Y4,Y5,Y6 such that
A40: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y
& Y1 meets X by A9;
Y in union union union union union union union union union X by A9,A39;
then Y6 in union union union union union union union union union union X
by A40,TARSKI:def 4;
then Y6 in ZA by A10,A40;
then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA by XBOOLE_0:def 2;
then Y6 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then Y6 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then Y6 in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then Y6 in (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD \/ ZE by XBOOLE_0:def 2;
then Y6 in V by XBOOLE_0:def 2;
hence contradiction by A18,A40,XBOOLE_0:3;
suppose
A41: Y in ZA;
then consider Y1,Y2,Y3,Y4,Y5 such that
A42: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in
Y & Y1 meets X by A10;
Y in union union union union union union union union union union X
by A10,A41;
then Y5 in union union union union union union union union union union
(union X)
by A42,TARSKI:def 4;
then Y5 in ZB by A11,A42;
then Y5 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
by XBOOLE_0:def 2;
then Y5 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
by XBOOLE_0:def 2;
then Y5 in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD by XBOOLE_0:def 2;
then Y5 in (X \/ Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB \/ ZC
\/ ZD \/ ZE by XBOOLE_0:def 2;
then Y5 in V by XBOOLE_0:def 2;
hence contradiction by A18,A42,XBOOLE_0:3;
suppose
A43: Y in ZB;
then consider Y1,Y2,Y3,Y4 such that
A44: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & Y1 meets X by A11;
Y in union union union union union union union union union union (union
X
)
by A11,A43;
then Y4 in union union union union union union union union union union
(union union X)
by A44,TARSKI:def 4;
then Y4 in ZC by A12,A44;
then Y4 in ((X \/ Z1) \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC by XBOOLE_0:def 2;
then Y4 in ((X \/ Z1) \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD by XBOOLE_0:def 2;
then Y4 in ((X \/ Z1) \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD \/ ZE by XBOOLE_0:def 2;
then Y4 in V by XBOOLE_0:def 2;
hence contradiction by A18,A44,XBOOLE_0:3;
suppose
A45: Y in ZC;
then consider Y1,Y2,Y3 such that
A46: Y1 in Y2 & Y2 in Y3 & Y3 in Y & Y1 meets X by A12;
Y in union union union union union union union union union union
(union union X) by A12,A45;
then Y3 in union union union union union union union union union union
(union union union X)
by A46,TARSKI:def 4;
then Y3 in ZD by A13,A46;
then Y3 in ((X \/ Z1) \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD by XBOOLE_0:def 2;
then Y3 in ((X \/ Z1) \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD \/ ZE by XBOOLE_0:def 2;
then Y3 in V by XBOOLE_0:def 2;
hence contradiction by A18,A46,XBOOLE_0:3;
suppose
A47: Y in ZD;
then consider Y1,Y2 such that
A48: Y1 in Y2 & Y2 in Y & Y1 meets X by A13;
Y in union union union union union union union union union union
(union union union X) by A13,A47;
then Y2 in union union union union union union union union union union
(union union union union X)
by A48,TARSKI:def 4;
then Y2 in ZE by A14,A48;
then Y2 in ((X \/ Z1) \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/
ZA \/ ZB
\/ ZC \/ ZD \/ ZE by XBOOLE_0:def 2;
then Y2 in V by XBOOLE_0:def 2;
hence contradiction by A18,A48,XBOOLE_0:3;
suppose
A49: Y in ZE;
then consider Y1 such that
A50: Y1 in Y & Y1 meets X by A14;
Y in union union union union union union union union union union
(union union union union X) by A14,A49;
then Y1 in union union union union union union union union union union
(union union union union union X) by A50,TARSKI:def 4;
then Y1 in ZF by A15,A50;
then Y1 in V by XBOOLE_0:def 2;
hence contradiction by A18,A50,XBOOLE_0:3;
suppose Y in ZF;
then Y meets X by A15;
hence contradiction by A16,A18,XBOOLE_1:70;
end;
::
:: Tuples for n=9
::
definition
let x1,x2,x3,x4,x5,x6,x7,x8,x9;
func [x1,x2,x3,x4,x5,x6,x7,x8,x9] equals
:Def1: [[x1,x2,x3,x4,x5,x6,x7,x8],x9];
correctness;
end;
theorem
Th3:[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 Def1
.= [[[x1,x2,x3,x4,x5,x6,x7],x8],x9] by MCART_5:def 1
.= [[[[x1,x2,x3,x4,x5,x6],x7],x8],x9] by MCART_4:def 1
.= [[[[[x1,x2,x3,x4,x5],x6],x7],x8],x9] by MCART_3:def 1
.= [[[[[[x1,x2,x3,x4],x5],x6],x7],x8],x9] by MCART_2:def 1
.= [[[[[[[x1,x2,x3],x4],x5],x6],x7],x8],x9] by MCART_1:def 4
.= [[[[[[[[x1,x2],x3],x4],x5],x6],x7],x8],x9] by MCART_1:def 3;
end;
canceled;
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 Th3
.= [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8,x9] by MCART_1:def 3
.= [[x1,x2,x3,x4,x5,x6,x7],x8,x9] by MCART_4:3;
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 Th3
.= [[[[[[x1,x2],x3],x4],x5],x6],x7,x8,x9] by MCART_1:31
.= [[x1,x2,x3,x4,x5,x6],x7,x8,x9] by MCART_3:3;
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 Th3
.= [[[[[x1,x2],x3],x4],x5],x6,x7,x8,x9] by MCART_2:3
.= [[x1,x2,x3,x4,x5],x6,x7,x8,x9] by MCART_2:3;
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 Th3
.= [[[[x1,x2],x3],x4],x5,x6,x7,x8,x9] by MCART_3:3
.= [[x1,x2,x3,x4],x5,x6,x7,x8,x9] by MCART_1:31;
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 Th3
.= [[[x1,x2],x3],x4,x5,x6,x7,x8,x9] by MCART_4:3
.= [[x1,x2,x3],x4,x5,x6,x7,x8,x9] by MCART_1:def 3;
end;
theorem
Th10: [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 Th3
.= [[[x1,x2],x3],x4,x5,x6,x7,x8,x9] by MCART_4:3
.= [[x1,x2],x3,x4,x5,x6,x7,x8,x9] by MCART_5:9;
end;
theorem
Th11:
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [y1,y2,y3,y4,y5,y6,y7,y8,y9]
implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6
& x7 = y7 & x8 = y8 & x9 =y9
proof
assume [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [y1,y2,y3,y4,y5,y6,y7,y8,y9];
then [[x1,x2,x3,x4,x5,x6,x7,x8],x9]
= [y1,y2,y3,y4,y5,y6,y7,y8,y9] by Def1
.= [[y1,y2,y3,y4,y5,y6,y7,y8],y9] by Def1;
then [x1,x2,x3,x4,x5,x6,x7,x8] = [y1,y2,y3,y4,y5,y6,y7,y8]
& x9 = y9 by ZFMISC_1:33;
hence thesis by MCART_5:10;
end;
::
:: Cartesian products of nine sets
::
definition
let X1,X2,X3,X4,X5,X6,X7,X8,X9;
func [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] -> set equals
:Def2: [:[: X1,X2,X3,X4,X5,X6,X7,X8 :],X9 :];
coherence;
end;
theorem
Th12:
[: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 Def2
.= [:[:[:X1,X2,X3,X4,X5,X6,X7:],X8:],X9:] by MCART_5:def 2
.= [:[:[:[:X1,X2,X3,X4,X5,X6:],X7:],X8:],X9:] by MCART_4:def 2
.= [:[:[:[:[:X1,X2,X3,X4,X5:],X6:],X7:],X8:],X9:] by MCART_3:def 2
.= [:[:[:[:[:[:X1,X2,X3,X4:],X5:],X6:],X7:],X8:],X9:] by MCART_2:def 2
.= [:[:[:[:[:[:[:X1,X2,X3:],X4:],X5:],X6:],X7:],X8:],X9:]by ZFMISC_1:def 4
.= [:[:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:],X9:]
by ZFMISC_1:def 3;
end;
canceled;
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 Th12
.= [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8,X9:]
by ZFMISC_1:def 3
.= [:[:X1,X2,X3,X4,X5,X6,X7:],X8,X9:] by MCART_4:11;
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 Th12
.= [:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7,X8,X9:] by MCART_1:53
.= [:[:X1,X2,X3,X4,X5,X6:],X7,X8,X9:] by MCART_3:10;
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 Th12
.= [:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6,X7,X8,X9:] by MCART_2:9
.= [:[:X1,X2,X3,X4,X5:],X6,X7,X8,X9:] by MCART_2:9;
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 Th12
.= [:[:[:[:X1,X2:],X3:],X4:],X5,X6,X7,X8,X9:] by MCART_3:10
.= [:[:X1,X2,X3,X4:],X5,X6,X7,X8,X9:] by MCART_1:53;
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 Th12
.= [:[:[:X1,X2:],X3:],X4,X5,X6,X7,X8,X9:] by MCART_4:11
.= [:[:X1,X2,X3:],X4,X5,X6,X7,X8,X9:] by ZFMISC_1:def 3;
end;
theorem
Th19: [: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 Th12
.= [:[:[:X1,X2:],X3:],X4,X5,X6,X7,X8,X9:] by MCART_4:11
.= [:[:X1,X2:],X3,X4,X5,X6,X7,X8,X9:] by MCART_5:18;
end;
theorem
Th20: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {}
& X7 <> {} & X8 <> {} & X9 <> {}
iff [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] <> {}
proof
A1: [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:] =
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] by Def2;
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
iff [:X1,X2,X3,X4,X5,X6,X7,X8:] <> {} by MCART_5:19;
hence thesis by A1,ZFMISC_1:113;
end;
theorem
Th21:
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>{}
implies
( [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:]
implies
X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 & X6=Y6 & X7=Y7 & X8=Y8 & X9=Y9)
proof
A1: [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] =
[:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:] by Def2;
assume
A2: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{};
then A3: [:X1,X2,X3,X4,X5,X6,X7,X8:] <> {} by MCART_5:19;
assume
A4: X9<>{};
assume [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] =
[:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:];
then [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:]
= [:[:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:],Y9:] by A1,Def2;
then [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:]
& X9 = Y9 by A3,A4,ZFMISC_1:134;
hence thesis by A2,MCART_5:20;
end;
theorem
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:]<>{}
& [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:]
implies
X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 & X6=Y6 & X7=Y7 & X8=Y8 & X9=Y9
proof
assume [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]<>{};
then X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{}
by Th20;
hence thesis by Th21;
end;
theorem
[:X,X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y,Y:] implies X = Y
proof
assume [:X,X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y,Y:];
then X<>{} or Y<>{} implies thesis by Th21;
hence X = Y;
end;
reserve xx9 for Element of X9;
theorem
Th24:
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>{}
implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
ex xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9]
proof
assume
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{};
then A2: [:X1,X2,X3,X4,X5,X6,X7,X8:] <> {} by MCART_5:19;
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
reconsider x'=x as
Element of [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:] by Def2;
consider x12345678 being (Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]),
xx9 such that
A3: x' = [x12345678,xx9] by A1,A2,MCART_2:36;
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that
A4: x12345678 = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,MCART_5:23;
take xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9;
thus x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A3,A4,Def1;
end;
definition
let X1,X2,X3,X4,X5,X6,X7,X8,X9;
assume
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{};
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
func x`1 -> Element of X1 means
:Def3: x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x1;
existence
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A2: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
take xx1;
thus thesis by A2,Th11;
end;
uniqueness
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A3: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
let y,z be Element of X1;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies y = x1;
then A4: y = xx1 by A3;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies z = x1;
hence thesis by A3,A4;
end;
func x`2 -> Element of X2 means
:Def4: x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x2;
existence
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A5: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
take xx2; thus thesis by A5,Th11;
end;
uniqueness
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A6: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
let y,z be Element of X2;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies y = x2;
then A7: y = xx2 by A6;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies z = x2;
hence thesis by A6,A7;
end;
func x`3 -> Element of X3 means
:Def5: x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x3;
existence
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A8: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
take xx3; thus thesis by A8,Th11;
end;
uniqueness
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A9: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
let y,z be Element of X3;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies y = x3;
then A10: y = xx3 by A9;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies z = x3;
hence thesis by A9,A10;
end;
func x`4 -> Element of X4 means
:Def6: x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x4;
existence
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A11: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
take xx4; thus thesis by A11,Th11;
end;
uniqueness
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A12: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
let y,z be Element of X4;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies y = x4;
then A13: y = xx4 by A12;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies z = x4;
hence thesis by A12,A13;
end;
func x`5 -> Element of X5 means
:Def7: x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x5;
existence
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A14: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
take xx5; thus thesis by A14,Th11;
end;
uniqueness
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A15: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
let y,z be Element of X5;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies y = x5;
then A16: y = xx5 by A15;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies z = x5;
hence thesis by A15,A16;
end;
func x`6 -> Element of X6 means
:Def8: x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x6;
existence
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A17: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
take xx6; thus thesis by A17,Th11;
end;
uniqueness
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A18: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
let y,z be Element of X6;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies y = x6;
then A19: y = xx6 by A18;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies z = x6;
hence thesis by A18,A19;
end;
func x`7 -> Element of X7 means
:Def9: x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x7;
existence
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A20: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
take xx7; thus thesis by A20,Th11;
end;
uniqueness
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A21: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
let y,z be Element of X7;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies y = x7;
then A22: y = xx7 by A21;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies z = x7;
hence thesis by A21,A22;
end;
func x`8 -> Element of X8 means
:Def10: x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x8;
existence
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A23: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
take xx8; thus thesis by A23,Th11;
end;
uniqueness
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A24: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
let y,z be Element of X8;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies y = x8;
then A25: y = xx8 by A24;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies z = x8;
hence thesis by A24,A25;
end;
func x`9 -> Element of X9 means
:Def11: x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x9;
existence
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A26: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
take xx9; thus thesis by A26,Th11;
end;
uniqueness
proof
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A27: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
let y,z be Element of X9;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies y = x9;
then A28: y = xx9 by A27;
assume x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies z = x9;
hence thesis by A27,A28;
end;
end;
theorem
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for x1,x2,x3,x4,x5,x6,x7,x8,x9
st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 & x`5 = x5 & x`6 = x6
& x`7 = x7 & x`8 = x8 & x`9 = x9
by Def3,Def4,Def5,Def6,Def7,Def8,Def9,Def10,Def11;
theorem Th26:
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>{}
implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
holds x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9]
proof
assume
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{};
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 such that
A2: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,Th24;
thus x = [x`1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,A2,Def3
.= [x`1,x`2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,A2,Def4
.= [x`1,x`2,x`3,xx4,xx5,xx6,xx7,xx8,xx9] by A1,A2,Def5
.= [x`1,x`2,x`3,x`4,xx5,xx6,xx7,xx8,xx9] by A1,A2,Def6
.= [x`1,x`2,x`3,x`4,x`5,xx6,xx7,xx8,xx9] by A1,A2,Def7
.= [x`1,x`2,x`3,x`4,x`5,x`6,xx7,xx8,xx9] by A1,A2,Def8
.= [x`1,x`2,x`3,x`4,x`5,x`6,x`7,xx8,xx9] by A1,A2,Def9
.= [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,xx9] by A1,A2,Def10
.= [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9] by A1,A2,Def11;
end;
theorem
Th27:
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>{}
implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds
x`1 = (x qua set)`1`1`1`1`1`1`1`1 &
x`2 = (x qua set)`1`1`1`1`1`1`1`2 &
x`3 = (x qua set)`1`1`1`1`1`1`2 &
x`4 = (x qua set)`1`1`1`1`1`2 &
x`5 = (x qua set)`1`1`1`1`2 &
x`6 = (x qua set)`1`1`1`2 &
x`7 = (x qua set)`1`1`2 &
x`8 = (x qua set)`1`2 &
x`9 = (x qua set)`2
proof
assume
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{};
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
thus x`1
= [ x`1, x`2]`1 by MCART_1:7
.= [[x`1, x`2],x`3]`1`1 by MCART_1:7
.= [ x`1, x`2 ,x`3]`1`1 by MCART_1:def 3
.= [[x`1, x`2 ,x`3],x`4]`1`1`1 by MCART_1:7
.= [ x`1, x`2 ,x`3 ,x`4]`1`1`1 by MCART_1:def 4
.= [[x`1, x`2 ,x`3 ,x`4], x`5]`1`1`1`1 by MCART_1:7
.= [ x`1, x`2 ,x`3 ,x`4 , x`5]`1`1`1`1 by MCART_2:def 1
.= [[x`1, x`2 ,x`3 ,x`4, x`5],x`6]`1`1`1`1`1 by MCART_1:7
.= [ x`1, x`2 ,x`3 ,x`4 ,x`5, x`6]`1`1`1`1`1 by MCART_3:def 1
.= [[x`1, x`2 ,x`3 ,x`4, x`5, x`6],x`7]`1`1`1`1`1`1 by MCART_1:7
.= [ x`1, x`2 ,x`3 ,x`4 ,x`5, x`6, x`7]`1`1`1`1`1`1 by MCART_4:def 1
.= [[x`1, x`2 ,x`3 ,x`4, x`5, x`6, x`7],x`8]`1`1`1`1`1`1`1 by MCART_1:7
.= [ x`1, x`2 ,x`3 ,x`4 ,x`5, x`6, x`7, x`8]`1`1`1`1`1`1`1 by MCART_5:def 1
.= [[x`1, x`2 ,x`3 ,x`4, x`5, x`6, x`7, x`8],x`9]`1`1`1`1`1`1`1`1 by MCART_1:7
.= [ x`1, x`2 ,x`3 ,x`4 ,x`5, x`6, x`7, x`8, x`9]`1`1`1`1`1`1`1`1 by Def1
.= (x qua set)`1`1`1`1`1`1`1`1 by A1,Th26;
thus x`2
= [ x`1, x`2]`2 by MCART_1:7
.= [[x`1, x`2],x`3]`1`2 by MCART_1:7
.= [ x`1, x`2, x`3]`1`2 by MCART_1:def 3
.= [[x`1, x`2, x`3],x`4]`1`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4]`1`1`2 by MCART_1:def 4
.= [[x`1, x`2, x`3, x`4 ], x`5]`1`1`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4 , x`5]`1`1`1`2 by MCART_2:def 1
.= [[x`1, x`2, x`3, x`4, x`5],x`6]`1`1`1`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4, x`5, x`6]`1`1`1`1`2 by MCART_3:def 1
.= [[x`1, x`2, x`3, x`4, x`5, x`6],x`7]`1`1`1`1`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4, x`5, x`6, x`7]`1`1`1`1`1`2 by MCART_4:def 1
.= [[x`1, x`2, x`3, x`4, x`5, x`6, x`7],x`8]`1`1`1`1`1`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4, x`5, x`6, x`7, x`8]`1`1`1`1`1`1`2 by MCART_5:def 1
.= [[x`1, x`2, x`3, x`4, x`5, x`6, x`7, x`8],x`9]`1`1`1`1`1`1`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4, x`5, x`6, x`7, x`8, x`9]`1`1`1`1`1`1`1`2 by Def1
.= (x qua set)`1`1`1`1`1`1`1`2 by A1,Th26;
thus x`3
= [[x`1, x`2],x`3]`2 by MCART_1:7
.= [ x`1, x`2, x`3]`2 by MCART_1:def 3
.= [[x`1, x`2, x`3],x`4]`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4]`1`2 by MCART_1:def 4
.= [[x`1, x`2, x`3, x`4],x`5]`1`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4 ,x`5]`1`1`2 by MCART_2:def 1
.= [[x`1, x`2, x`3, x`4, x`5],x`6]`1`1`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4, x`5, x`6]`1`1`1`2 by MCART_3:def 1
.= [[x`1, x`2, x`3, x`4, x`5, x`6],x`7]`1`1`1`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4, x`5, x`6, x`7]`1`1`1`1`2 by MCART_4:def 1
.= [[x`1, x`2, x`3, x`4, x`5, x`6, x`7],x`8]`1`1`1`1`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4, x`5, x`6, x`7, x`8]`1`1`1`1`1`2 by MCART_5:def 1
.= [[x`1, x`2, x`3, x`4, x`5, x`6, x`7, x`8],x`9]`1`1`1`1`1`1`2 by MCART_1:7
.= [ x`1, x`2, x`3, x`4, x`5, x`6, x`7, x`8, x`9]`1`1`1`1`1`1`2 by Def1
.= (x qua set)`1`1`1`1`1`1`2 by A1,Th26;
thus x`4
= [[x`1,x`2,x`3],x`4]`2 by MCART_1:7
.= [ x`1,x`2,x`3, x`4]`2 by MCART_1:def 4
.= [[x`1,x`2,x`3, x`4],x`5]`1`2 by MCART_1:7
.= [ x`1,x`2,x`3, x`4 ,x`5]`1`2 by MCART_2:def 1
.= [[x`1,x`2,x`3, x`4, x`5],x`6]`1`1`2 by MCART_1:7
.= [ x`1,x`2,x`3, x`4, x`5, x`6]`1`1`2 by MCART_3:def 1
.= [[x`1,x`2,x`3, x`4, x`5, x`6],x`7]`1`1`1`2 by MCART_1:7
.= [ x`1,x`2,x`3, x`4, x`5, x`6, x`7]`1`1`1`2 by MCART_4:def 1
.= [[x`1,x`2,x`3, x`4, x`5, x`6, x`7],x`8]`1`1`1`1`2 by MCART_1:7
.= [ x`1,x`2,x`3, x`4, x`5, x`6, x`7, x`8]`1`1`1`1`2 by MCART_5:def 1
.= [[x`1,x`2,x`3, x`4, x`5, x`6, x`7, x`8],x`9]`1`1`1`1`1`2 by MCART_1:7
.= [ x`1,x`2,x`3, x`4, x`5, x`6, x`7, x`8, x`9]`1`1`1`1`1`2 by Def1
.= (x qua set)`1`1`1`1`1`2 by A1,Th26;
thus x`5
= [[x`1,x`2,x`3,x`4],x`5]`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4 ,x`5]`2 by MCART_2:def 1
.= [[x`1,x`2,x`3,x`4,x`5],x`6]`1`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5, x`6]`1`2 by MCART_3:def 1
.= [[x`1,x`2,x`3,x`4,x`5,x`6],x`7]`1`1`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5, x`6,x`7]`1`1`2 by MCART_4:def 1
.= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7],x`8]`1`1`1`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5, x`6,x`7,x`8]`1`1`1`2 by MCART_5:def 1
.= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8],x`9]`1`1`1`1`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8, x`9]`1`1`1`1`2 by Def1
.= (x qua set)`1`1`1`1`2 by A1,Th26;
thus x`6
= [[x`1,x`2,x`3,x`4,x`5],x`6]`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5, x`6]`2 by MCART_3:def 1
.= [[x`1,x`2,x`3,x`4,x`5,x`6],x`7]`1`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5,x`6, x`7]`1`2 by MCART_4:def 1
.= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7],x`8]`1`1`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5,x`6,x`7, x`8]`1`1`2 by MCART_5:def 1
.= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7, x`8],x`9]`1`1`1`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5,x`6,x`7, x`8, x`9]`1`1`1`2 by Def1
.= (x qua set)`1`1`1`2 by A1,Th26;
thus x`7
= [[x`1,x`2,x`3,x`4,x`5,x`6],x`7]`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5,x`6, x`7]`2 by MCART_4:def 1
.= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7],x`8]`1`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5,x`6,x`7, x`8]`1`2 by MCART_5:def 1
.= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8],x`9]`1`1`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8, x`9]`1`1`2 by Def1
.= (x qua set)`1`1`2 by A1,Th26;
thus x`8
= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7],x`8]`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5,x`6,x`7, x`8]`2 by MCART_5:def 1
.= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8],x`9]`1`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8, x`9]`1`2 by Def1
.= (x qua set)`1`2 by A1,Th26;
thus x`9
= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8],x`9]`2 by MCART_1:7
.= [ x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8, x`9]`2 by Def1
.= (x qua set)`2 by A1,Th26;
end;
theorem
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] implies
X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5
& X6 meets Y6 & X7 meets Y7 & X8 meets Y8 & X9 meets Y9
proof
A1: [:[:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:],X9:]
= [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
& [:[:[:[:[:[:[:[:Y1,Y2:],Y3:],Y4:],Y5:],Y6:],Y7:],Y8:],Y9:]
= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] by Th12;
A2: [:X1,X2,X3,X4,X5,X6,X7,X8:] =
[:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:]
& [:[:[:[:[:[:[:Y1,Y2:],Y3:],Y4:],Y5:],Y6:],Y7:],Y8:]
= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] by MCART_5:12;
assume [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:];
then [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:] meets
[:[:[:[:[:[:[:Y1,Y2:],Y3:],Y4:],Y5:],Y6:],Y7:],Y8:]
& X9 meets Y9 by A1,ZFMISC_1:127;
hence thesis by A2,MCART_5:28;
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 Th19
.= [:{[x1,x2]}, {x3},{x4},{x5},{x6},{x7},{x8},{x9}:] by ZFMISC_1:35
.= { [[x1,x2], x3, x4, x5, x6, x7, x8, x9]} by MCART_5:29
.= { [x1,x2,x3,x4,x5,x6,x7,x8,x9] } by Th10;
end;
reserve A1 for Subset of X1,
A2 for Subset of X2,
A3 for Subset of X3,
A4 for Subset of X4,
A5 for Subset of X5,
A6 for Subset of X6,
A7 for Subset of X7,
A8 for Subset of X8,
A9 for Subset of X9;
:: 9 - Tuples
reserve x for Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
theorem
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
implies
for x1,x2,x3,x4,x5,x6,x7,x8,x9 st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9]
holds x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 & x`5 = x5
& x`6 = x6 & x`7 = x7 & x`8 = x8 & x`9 = x9 by Def3,Def4,Def5,Def6,Def7,
Def8,Def9,Def10,Def11;
theorem
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y1 = xx1)
implies y1 =x`1
proof
assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{} and
A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y1 = xx1;
x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9] by A1,Th26;
hence thesis by A2;
end;
theorem
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y2 = xx2)
implies y2 =x`2
proof
assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{} and
A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y2 = xx2;
x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9] by A1,Th26;
hence thesis by A2;
end;
theorem
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y3 = xx3)
implies y3 =x`3
proof
assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{} and
A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y3 = xx3;
x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9] by A1,Th26;
hence thesis by A2;
end;
theorem
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y4 = xx4)
implies y4 =x`4
proof
assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{} and
A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y4 = xx4;
x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9] by A1,Th26;
hence thesis by A2;
end;
theorem
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y5 = xx5)
implies y5 =x`5
proof
assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{} and
A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y5 = xx5;
x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9] by A1,Th26;
hence thesis by A2;
end;
theorem
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y6 = xx6)
implies y6 =x`6
proof
assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{} and
A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y6 = xx6;
x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9] by A1,Th26;
hence thesis by A2;
end;
theorem
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y7 = xx7)
implies y7 =x`7
proof
assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{} and
A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y7 = xx7;
x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9] by A1,Th26;
hence thesis by A2;
end;
theorem
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y8 = xx8)
implies y8 =x`8
proof
assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{} and
A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y8 = xx8;
x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9] by A1,Th26;
hence thesis by A2;
end;
theorem
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y9 = xx9)
implies y9 =x`9
proof
assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{} and
A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y9 = xx9;
x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9] by A1,Th26;
hence thesis by A2;
end;
theorem
y in [: X1,X2,X3,X4,X5,X6,X7,X8,X9 :] implies
ex x1,x2,x3,x4,x5,x6,x7,x8,x9
st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
& x6 in X6 & x7 in X7 & x8 in X8 & x9 in X9
& y = [x1,x2,x3,x4,x5,x6,x7,x8,x9]
proof
assume y in [: X1,X2,X3,X4,X5,X6,X7,X8,X9 :];
then y in [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:] by Def2;
then consider x12345678, x9 being set such that
A1: x12345678 in [:X1,X2,X3,X4,X5,X6,X7,X8:] and
A2: x9 in X9 and
A3: y = [x12345678,x9] by ZFMISC_1:def 2;
consider x1, x2, x3, x4, x5, x6, x7, x8 such that
A4: x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4
& x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8
& x12345678 = [x1,x2,x3,x4,x5,x6,x7,x8] by A1,MCART_5:39;
y = [x1,x2,x3,x4,x5,x6,x7,x8,x9] by A3,A4,Def1;
hence thesis by A2,A4;
end;
theorem
[x1,x2,x3,x4,x5,x6,x7,x8,x9] in [: X1,X2,X3,X4,X5,X6,X7,X8,X9 :]
iff x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
& x6 in X6 & x7 in X7 & x8 in X8 & x9 in X9
proof
A1: [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
= [:[:X1,X2:],X3,X4,X5,X6,X7,X8,X9:] by Th19;
A2: [x1,x2,x3,x4,x5,x6,x7,x8,x9]
= [[x1,x2],x3,x4,x5,x6,x7,x8,x9] by Th10;
[x1,x2] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:106;
hence thesis by A1,A2,MCART_5:40;
end;
theorem
(for y holds y in Z iff
ex x1,x2,x3,x4,x5,x6,x7,x8,x9
st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
& x6 in X6 & x7 in X7 & x8 in X8 & x9 in X9
& y = [x1,x2,x3,x4,x5,x6,x7,x8,x9])
implies Z = [: X1,X2,X3,X4,X5,X6,X7,X8,X9 :]
proof
assume
A1: for y holds y in Z iff
ex x1,x2,x3,x4,x5,x6,x7,x8,x9
st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
& x6 in X6 & x7 in X7 & x8 in X8 & x9 in X9
& y = [x1,x2,x3,x4,x5,x6,x7,x8,x9];
now let y;
thus y in Z implies y in [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:]
proof
assume y in Z; then consider x1,x2,x3,x4,x5,x6,x7,x8,x9 such that
A2: x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
& x6 in X6 & x7 in X7 & x8 in X8 & x9 in X9
& y = [x1,x2,x3,x4,x5,x6,x7,x8,x9] by A1;
A3: y = [[x1,x2,x3,x4,x5,x6,x7,x8],x9] by A2,Def1;
[x1,x2,x3,x4,x5,x6,x7,x8] in [:X1,X2,X3,X4,X5,X6,X7,X8:]
& x9 in X9 by A2,MCART_5:40;
hence y in [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:] by A3,ZFMISC_1:def 2;
end;
assume y in [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:];
then consider x12345678,x9 being set such that
A4: x12345678 in [:X1,X2,X3,X4,X5,X6,X7,X8:] and
A5: x9 in X9 and
A6: y = [x12345678,x9] by ZFMISC_1:def 2;
consider x1,x2,x3,x4,x5,x6,x7,x8 such that
A7: x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 &
x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8
& x12345678 = [x1,x2,x3,x4,x5,x6,x7,x8] by A4,MCART_5:39;
y = [x1,x2,x3,x4,x5,x6,x7,x8,x9] by A6,A7,Def1;
hence y in Z by A1,A5,A7;
end;
then Z = [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:] by TARSKI:2;
hence Z = [: X1,X2,X3,X4,X5,X6,X7,X8,X9 :] by Def2;
end;
theorem Th43:
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
& Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} & Y5<>{} & Y6<>{} & Y7<>{} & Y8<>{} & Y9<>
{}
implies
for x being (Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]),
y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:]
holds x = y
implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3 & x`4 = y`4 & x`5 = y`5
& x`6 = y`6 & x`7 = y`7 & x`8 = y`8 & x`9 = y`9
proof
assume that
A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{} and
A2: Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} & Y5<>{} & Y6<>{} & Y7<>{} & Y8<>{}
& Y9<>{};
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
let y be Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:];
assume
A3: x = y;
thus x`1 = (x qua set)`1`1`1`1`1`1`1`1 by A1,Th27 .= y`1 by A2,A3,Th27;
thus x`2 = (x qua set)`1`1`1`1`1`1`1`2 by A1,Th27 .= y`2 by A2,A3,Th27;
thus x`3 = (x qua set)`1`1`1`1`1`1`2 by A1,Th27 .= y`3 by A2,A3,Th27;
thus x`4 = (x qua set)`1`1`1`1`1`2 by A1,Th27 .= y`4 by A2,A3,Th27;
thus x`5 = (x qua set)`1`1`1`1`2 by A1,Th27 .= y`5 by A2,A3,Th27;
thus x`6 = (x qua set)`1`1`1`2 by A1,Th27 .= y`6 by A2,A3,Th27;
thus x`7 = (x qua set)`1`1`2 by A1,Th27 .= y`7 by A2,A3,Th27;
thus x`8 = (x qua set)`1`2 by A1,Th27 .= y`8 by A2,A3,Th27;
thus x`9 = (x qua set)`2 by A1,Th27 .= y`9 by A2,A3,Th27;
end;
theorem
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:]
holds x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4 & x`5 in A5
& x`6 in A6 & x`7 in A7 & x`8 in A8 & x`9 in A9
proof
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
assume
A1: x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:];
then A2: A1<>{} & A2<>{} & A3<>{} & A4<>{} & A5<>{} & A6<>{} & A7<>{} & A8<>
{}
& A9<>{}
by Th20;
reconsider y = x as
Element of [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] by A1;
y`1 in A1 & y`2 in A2 & y`3 in A3 & y`4 in A4 & y`5 in A5
& y`6 in A6 & y`7 in A7 & y`8 in A8 & y`9 in A9 by A2;
hence x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4 & x`5 in A5
& x`6 in A6 & x`7 in A7 & x`8 in A8 & x`9 in A9 by Th43;
end;
theorem Th45:
X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 & X6 c= Y6 & X7 c= Y7
& X8 c= Y8 & X9 c= Y9
implies [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:]
proof
assume X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5
& X6 c= Y6 & X7 c= Y7 & X8 c= Y8;
then A1: [:X1,X2,X3,X4,X5,X6,X7,X8:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] by
MCART_5:44;
A2: [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
= [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:] &
[:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:]
= [:[:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:],Y9:] by Def2;
assume X9 c= Y9;
hence thesis by A1,A2,ZFMISC_1:119;
end;
theorem
[:A1,A2,A3,A4,A5,A6,A7,A8,A9:] is Subset of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
by Th45;