### The Mizar article:

### $N$-Tuples and Cartesian Products for $n=5$

**by****Michal Muzalewski, and****Wojciech Skaba**

- Received October 13, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: MCART_2
- [ MML identifier index ]

environ vocabulary BOOLE, MCART_1, TARSKI, MCART_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1; constructors TARSKI, MCART_1, MEMBERED, XBOOLE_0; clusters MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; theorems TARSKI, ZFMISC_1, MCART_1, XBOOLE_0, XBOOLE_1; schemes XBOOLE_0; begin reserve x,x1,x2,x3,x4,x5, y,y1,y2,y3,y4,y5, X,X1,X2,X3,X4,X5, Y,Y1,Y2,Y3,Y4,Y5,Y6,Y7, Z,Z1,Z2,Z3,Z4,Z5,Z6,Z7 for set; reserve xx1 for Element of X1, xx2 for Element of X2, xx3 for Element of X3, xx4 for Element of X4, xx5 for Element of X5; Lm1: X1 <> {} & X2 <> {} implies for x being Element of [:X1,X2:] ex xx1 being (Element of X1), xx2 being Element of X2 st x = [xx1,xx2] proof assume A1: X1 <> {} & X2 <> {}; then A2: [:X1,X2:] <> {} by ZFMISC_1:113; let x be Element of [:X1,X2:]; reconsider xx1 = x`1 as Element of X1 by A2,MCART_1:10; reconsider xx2 = x`2 as Element of X2 by A2,MCART_1:10; take xx1,xx2; thus x = [xx1,xx2] by A1,MCART_1:24; end; Lm2: X1 <> {} & X2 <> {} & X3 <> {} implies for x being Element of [:X1,X2,X3:] ex xx1,xx2,xx3 st x = [xx1,xx2,xx3] proof assume A1: X1 <> {} & X2 <> {} & X3 <> {}; then A2: [:X1,X2:] <> {} by ZFMISC_1:113; let x be Element of [:X1,X2,X3:]; reconsider x'=x as Element of [:[:X1,X2:],X3:] by ZFMISC_1:def 3; consider x12 being (Element of [:X1,X2:]), xx3 such that A3: x' = [x12,xx3] by A1,A2,Lm1; consider xx1,xx2 such that A4: x12 = [xx1,xx2] by A1,Lm1; take xx1,xx2,xx3; thus x = [xx1,xx2,xx3] by A3,A4,MCART_1:def 3; end; Lm3: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} implies for x being Element of [:X1,X2,X3,X4:] ex xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] proof assume A1: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {}; then A2: [:X1,X2,X3:] <> {} by MCART_1:35; let x be Element of [:X1,X2,X3,X4:]; reconsider x'=x as Element of [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4; consider x123 being (Element of [:X1,X2,X3:]), xx4 such that A3: x' = [x123,xx4] by A1,A2,Lm1; consider xx1,xx2,xx3 such that A4: x123 = [xx1,xx2,xx3] by A1,Lm2; take xx1,xx2,xx3,xx4; thus x = [xx1,xx2,xx3,xx4] by A3,A4,MCART_1:def 4; end; theorem X <> {} implies ex Y st Y in X & for Y1,Y2,Y3,Y4,Y5,Y6 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y holds Y1 misses X proof defpred P[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 Z1 such that A1: for Y holds Y in Z1 iff Y in union X & P[Y] from Separation; defpred Q[set] means ex Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in $1 & Y1 meets X; consider Z2 such that A2: for Y holds Y in Z2 iff Y in union union X & Q[Y] from Separation; defpred R[set] means ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X; consider Z3 such that A3: for Y holds Y in Z3 iff Y in union union union X & R[Y] from Separation; defpred S[set] means ex Y1,Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X; consider Z4 such that A4: for Y holds Y in Z4 iff Y in union union union union X & S[Y] from Separation; defpred T[set] means ex Y1 st Y1 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 & T[Y] from Separation; defpred U[set] means $1 meets X; consider Z6 such that A6: for Y holds Y in Z6 iff Y in union union union union union union X & U[Y] from Separation; set V = X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6; A7: V = X \/ (Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) by XBOOLE_1:4; assume X <> {}; then V <> {} by A7,XBOOLE_1:15; then consider Y such that A8: Y in V and A9: Y misses V by MCART_1:1; assume A10: not thesis; now assume A11: Y in X; then consider Y1,Y2,Y3,Y4,Y5,Y6 such that A12: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y & not Y1 misses X by A10; Y6 in union X & Y1 meets X by A11,A12,TARSKI:def 4; then Y6 in Z1 by A1,A12; then Y6 in X \/ Z1 by XBOOLE_0:def 2; then Y6 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then Y6 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by A12,XBOOLE_0:3; then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_1:70; hence contradiction by A9,XBOOLE_1:70; end; then Y in Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by A7,A8,XBOOLE_0:def 2; then Y in Z1 \/ (Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:4; then Y in Z1 \/ (Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 by XBOOLE_1:4; then Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 by XBOOLE_1:4; then A13: Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) by XBOOLE_1:4; now assume A14: Y in Z1; then consider Y1,Y2,Y3,Y4,Y5 such that A15: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y & Y1 meets X by A1; Y in union X by A1,A14; then Y5 in union union X by A15,TARSKI:def 4; then Y5 in Z2 by A2,A15; then Y5 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 by A15,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; hence contradiction by A9,XBOOLE_1:70; end; then Y in Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by A13,XBOOLE_0:def 2; then Y in Z2 \/ (Z3 \/ Z4) \/ Z5 \/ Z6 by XBOOLE_1:4; then Y in Z2 \/ (Z3 \/ Z4 \/ Z5) \/ Z6 by XBOOLE_1:4; then A16: Y in Z2 \/ (Z3 \/ Z4 \/ Z5 \/ Z6) by XBOOLE_1:4; now assume A17: Y in Z2; then consider Y1,Y2,Y3,Y4 such that A18: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & Y1 meets X by A2; Y in union union X by A2,A17; then Y4 in union union union X by A18,TARSKI:def 4; then Y4 in Z3 by A3,A18; then Y4 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y4 in V by XBOOLE_0:def 2; hence contradiction by A9,A18,XBOOLE_0:3; end; then Y in Z3 \/ Z4 \/ Z5 \/ Z6 by A16,XBOOLE_0:def 2; then Y in Z3 \/ (Z4 \/ Z5) \/ Z6 by XBOOLE_1:4; then A19: Y in Z3 \/ (Z4 \/ Z5 \/ Z6) by XBOOLE_1:4; now assume A20: Y in Z3; then consider Y1,Y2,Y3 such that A21: Y1 in Y2 & Y2 in Y3 & Y3 in Y & Y1 meets X by A3; Y in union union union X by A3,A20; then Y3 in union union union union X by A21,TARSKI:def 4; then Y3 in Z4 by A4,A21; then Y3 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then Y3 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y3 in V by XBOOLE_0:def 2; hence contradiction by A9,A21,XBOOLE_0:3; end; then Y in Z4 \/ Z5 \/ Z6 by A19,XBOOLE_0:def 2; then A22: Y in Z4 \/ (Z5 \/ Z6) by XBOOLE_1:4; now assume A23: Y in Z4; then consider Y1,Y2 such that A24: Y1 in Y2 & Y2 in Y & Y1 meets X by A4; Y in union union union union X by A4,A23; then Y2 in union union union union union X by A24,TARSKI:def 4; then Y2 in Z5 by A5,A24; then Y2 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y2 in V by XBOOLE_0:def 2; hence contradiction by A9,A24,XBOOLE_0:3; end; then A25: Y in Z5 \/ Z6 by A22,XBOOLE_0:def 2; now assume A26: Y in Z5; then consider Y1 such that A27: Y1 in Y & Y1 meets X by A5; Y in union union union union union X by A5,A26; then Y1 in union union union union union union X by A27,TARSKI:def 4; then Y1 in Z6 by A6,A27; then Y1 in V by XBOOLE_0:def 2; hence contradiction by A9,A27,XBOOLE_0:3; end; then Y in Z6 by A25,XBOOLE_0:def 2; then Y meets X by A6; hence contradiction by A7,A9,XBOOLE_1:70; end; theorem Th2: X <> {} implies ex Y st Y in X & for 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 Y holds Y1 misses X proof defpred P[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 Z1 such that A1: for Y holds Y in Z1 iff Y in union X & P[Y] from Separation; defpred Q[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 Z2 such that A2: for Y holds Y in Z2 iff Y in union union X & Q[Y] from Separation; defpred R[set] means ex Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in $1 & Y1 meets X; consider Z3 such that A3: for Y holds Y in Z3 iff Y in union union union X & R[Y] from Separation; defpred S[set] means ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X; consider Z4 such that A4: for Y holds Y in Z4 iff Y in union union union union X & S[Y] from Separation; defpred T[set] means ex Y1,Y2 st Y1 in Y2 & Y2 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 & T[Y] from Separation; defpred U[set] means ex Y1 st Y1 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 & U[Y] from Separation; defpred V[set] means $1 meets X; consider Z7 such that A7: for Y holds Y in Z7 iff Y in union union union union union union union X & V[Y] from Separation; set V = X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7; A8: V = X \/ (Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7) by XBOOLE_1:4; assume X <> {}; then V <> {} by A8,XBOOLE_1:15; then consider Y such that A9: Y in V and A10: Y misses V by MCART_1:1; assume A11: not thesis; now assume A12: Y in X; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7 such that A13: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y & not Y1 misses X by A11; Y7 in union X & Y1 meets X by A12,A13,TARSKI:def 4; then Y7 in Z1 by A1,A13; then Y7 in X \/ Z1 by XBOOLE_0:def 2; then Y7 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then Y7 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by A13,XBOOLE_0:3; then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_1:70; hence contradiction by A10,XBOOLE_1:70; end; then Y in Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by A8,A9,XBOOLE_0:def 2; then Y in Z1 \/ (Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4; then Y in Z1 \/ (Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4; then Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 by XBOOLE_1:4; then Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 by XBOOLE_1:4; then A14: Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7) by XBOOLE_1:4; now assume A15: Y in Z1; then consider Y1,Y2,Y3,Y4,Y5,Y6 such that A16: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y & Y1 meets X by A1; Y in union X by A1,A15; then Y6 in union union X by A16,TARSKI:def 4; then Y6 in Z2 by A2,A16; then Y6 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 by A16,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; hence contradiction by A10,XBOOLE_1:70; end; then Y in Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by A14,XBOOLE_0:def 2; then Y in Z2 \/ (Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 by XBOOLE_1:4; then Y in Z2 \/ (Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 by XBOOLE_1:4; then Y in Z2 \/ (Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 by XBOOLE_1:4; then A17: Y in Z2 \/ (Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7) by XBOOLE_1:4; now assume A18: Y in Z2; then consider Y1,Y2,Y3,Y4,Y5 such that A19: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y & Y1 meets X by A2; Y in union union X by A2,A18; then Y5 in union union union X by A19,TARSKI:def 4; then Y5 in Z3 by A3,A19; then Y5 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then Y5 in V by XBOOLE_0:def 2; hence contradiction by A10,A19,XBOOLE_0:3; end; then Y in Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by A17,XBOOLE_0:def 2; then Y in Z3 \/ (Z4 \/ Z5) \/ Z6 \/ Z7 by XBOOLE_1:4; then Y in Z3 \/ (Z4 \/ Z5 \/ Z6) \/ Z7 by XBOOLE_1:4; then A20: Y in Z3 \/ (Z4 \/ Z5 \/ Z6 \/ Z7) by XBOOLE_1:4; now assume A21: Y in Z3; then consider Y1,Y2,Y3,Y4 such that A22: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & Y1 meets X by A3; Y in union union union X by A3,A21; then Y4 in union union union union X by A22,TARSKI:def 4; then Y4 in Z4 by A4,A22; then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then Y4 in V by XBOOLE_0:def 2; hence contradiction by A10,A22,XBOOLE_0:3; end; then Y in Z4 \/ Z5 \/ Z6 \/ Z7 by A20,XBOOLE_0:def 2; then Y in Z4 \/ (Z5 \/ Z6) \/ Z7 by XBOOLE_1:4; then A23: Y in Z4 \/ (Z5 \/ Z6 \/ Z7) by XBOOLE_1:4; now assume A24: Y in Z4; then consider Y1,Y2,Y3 such that A25: Y1 in Y2 & Y2 in Y3 & Y3 in Y & Y1 meets X by A4; Y in union union union union X by A4,A24; then Y3 in union union union union union X by A25,TARSKI:def 4; then Y3 in Z5 by A5,A25; then Y3 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y3 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then Y3 in V by XBOOLE_0:def 2; hence contradiction by A10,A25,XBOOLE_0:3; end; then Y in Z5 \/ Z6 \/ Z7 by A23,XBOOLE_0:def 2; then A26: Y in Z5 \/ (Z6 \/ Z7) by XBOOLE_1:4; now assume A27: Y in Z5; then consider Y1,Y2 such that A28: Y1 in Y2 & Y2 in Y & Y1 meets X by A5; Y in union union union union union X by A5,A27; then Y2 in union union union union union union X by A28,TARSKI:def 4; then Y2 in Z6 by A6,A28; then Y2 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then Y2 in V by XBOOLE_0:def 2; hence contradiction by A10,A28,XBOOLE_0:3; end; then A29: Y in Z6 \/ Z7 by A26,XBOOLE_0:def 2; now assume A30: Y in Z6; then consider Y1 such that A31: Y1 in Y & Y1 meets X by A6; Y in union union union union union union X by A6,A30; then Y1 in union union union union union union union X by A31,TARSKI:def 4; then Y1 in Z7 by A7,A31; then Y1 in V by XBOOLE_0:def 2; hence contradiction by A10,A31,XBOOLE_0:3; end; then Y in Z7 by A29,XBOOLE_0:def 2; then Y meets X by A7; hence contradiction by A8,A10,XBOOLE_1:70; end; :: :: Tuples for n=5 :: definition let x1,x2,x3,x4,x5; func [x1,x2,x3,x4,x5] equals :Def1: [[x1,x2,x3,x4],x5]; correctness; end; theorem Th3: [x1,x2,x3,x4,x5] = [[[[x1,x2],x3],x4],x5] proof thus [x1,x2,x3,x4,x5] = [[x1,x2,x3,x4],x5] by Def1 .= [[[x1,x2,x3],x4],x5] by MCART_1:def 4 .= [[[[x1,x2],x3],x4],x5] by MCART_1:def 3; end; canceled; theorem [x1,x2,x3,x4,x5] = [[x1,x2,x3],x4,x5] proof thus [x1,x2,x3,x4,x5] = [[[[x1,x2],x3],x4],x5] by Th3 .= [[[x1,x2],x3],x4,x5] by MCART_1:def 3 .= [[x1,x2,x3],x4,x5] by MCART_1:def 3; end; theorem Th6: [x1,x2,x3,x4,x5] = [[x1,x2],x3,x4,x5] proof thus [x1,x2,x3,x4,x5] = [[[[x1,x2],x3],x4],x5] by Th3 .= [[[x1,x2],x3],x4,x5] by MCART_1:def 3 .= [[x1,x2],x3,x4,x5] by MCART_1:32; end; theorem Th7: [x1,x2,x3,x4,x5] = [y1,y2,y3,y4,y5] implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 proof assume [x1,x2,x3,x4,x5] = [y1,y2,y3,y4,y5]; then [[x1,x2,x3,x4],x5] = [y1,y2,y3,y4,y5] by Def1 .= [[y1,y2,y3,y4],y5] by Def1; then [x1,x2,x3,x4] = [y1,y2,y3,y4] & x5 = y5 by ZFMISC_1:33; hence thesis by MCART_1:33; end; theorem Th8: X <> {} implies ex x st x in X & not ex x1,x2,x3,x4,x5 st (x1 in X or x2 in X) & x = [x1,x2,x3,x4,x5] proof assume X <> {}; then consider Y such that A1: Y in X and A2: for 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 Y holds Y1 misses X by Th2; take x = Y; thus x in X by A1; given x1,x2,x3,x4,x5 such that A3: x1 in X or x2 in X and A4: x = [x1,x2,x3,x4,x5]; set Y1 = { x1, x2 }, Y2 = { Y1, {x1} }, Y3 = { Y2, x3 }, Y4 = { Y3, {Y2} }, Y5 = { Y4, x4 }, Y6 = { Y5, {Y4} }, Y7 = { Y6, x5 }; x1 in Y1 & x2 in Y1 by TARSKI:def 2; then A5: not Y1 misses X by A3,XBOOLE_0:3; Y = [[[[x1,x2],x3],x4],x5] by A4,Th3 .= [[[ Y2,x3],x4],x5 ] by TARSKI:def 5 .= [[ Y4,x4],x5 ] by TARSKI:def 5 .= [ Y6,x5 ] by TARSKI:def 5 .= { Y7, { Y6 } } by TARSKI:def 5; then Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y by TARSKI:def 2; hence contradiction by A2,A5; end; :: :: Cartesian products of five sets :: definition let X1,X2,X3,X4,X5; func [:X1,X2,X3,X4,X5:] -> set equals :Def2: [:[: X1,X2,X3,X4 :],X5 :]; correctness; end; theorem Th9: [:X1,X2,X3,X4,X5:] = [:[:[:[:X1,X2:],X3:],X4:],X5:] proof thus [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3,X4:],X5:] by Def2 .= [:[:[:X1,X2,X3:],X4:],X5:] by ZFMISC_1:def 4 .= [:[:[:[:X1,X2:],X3:],X4:],X5:] by ZFMISC_1:def 3; end; canceled; theorem [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3:],X4,X5:] proof thus [:X1,X2,X3,X4,X5:] = [:[:[:[:X1,X2:],X3:],X4:],X5:] by Th9 .= [:[:[:X1,X2:],X3:],X4,X5:] by ZFMISC_1:def 3 .= [:[:X1,X2,X3:],X4,X5:] by ZFMISC_1:def 3; end; theorem Th12: [:X1,X2,X3,X4,X5:] = [:[:X1,X2:],X3,X4,X5:] proof thus [:X1,X2,X3,X4,X5:] = [:[:[:[:X1,X2:],X3:],X4:],X5:] by Th9 .= [:[:[:X1,X2:],X3:],X4,X5:] by ZFMISC_1:def 3 .= [:[:X1,X2:],X3,X4,X5:] by MCART_1:54; end; theorem Th13: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} iff [:X1,X2,X3,X4,X5:] <> {} proof A1: [:[:X1,X2,X3,X4:],X5:] = [:X1,X2,X3,X4,X5:] by Def2; X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} iff [:X1,X2,X3,X4:] <> {} by MCART_1:55; hence thesis by A1,ZFMISC_1:113; end; theorem Th14: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} implies ( [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 ) proof A1: [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3,X4:],X5:] by Def2; assume A2: X1<>{} & X2<>{} & X3<>{} & X4<>{}; then A3: [:X1,X2,X3,X4:] <> {} by MCART_1:55; assume A4: X5<>{}; assume [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:]; then [:[:X1,X2,X3,X4:],X5:] = [:[:Y1,Y2,Y3,Y4:],Y5:] by A1,Def2; then [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] & X5 = Y5 by A3,A4,ZFMISC_1:134; hence thesis by A2,MCART_1:56; end; theorem [:X1,X2,X3,X4,X5:]<>{} & [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 proof assume [:X1,X2,X3,X4,X5:]<>{}; then X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} by Th13; hence thesis by Th14; end; theorem [:X,X,X,X,X:] = [:Y,Y,Y,Y,Y:] implies X = Y proof assume [:X,X,X,X,X:] = [:Y,Y,Y,Y,Y:]; then X<>{} or Y<>{} implies thesis by Th14; hence X = Y; end; theorem Th17: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} implies for x being Element of [:X1,X2,X3,X4,X5:] ex xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] proof assume A1: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {}; then A2: [:X1,X2,X3,X4:] <> {} by MCART_1:55; let x be Element of [:X1,X2,X3,X4,X5:]; reconsider x'=x as Element of [:[:X1,X2,X3,X4:],X5:] by Def2; consider x1234 being (Element of [:X1,X2,X3,X4:]), xx5 such that A3: x' = [x1234,xx5] by A1,A2,Lm1; consider xx1,xx2,xx3,xx4 such that A4: x1234 = [xx1,xx2,xx3,xx4] by A1,Lm3; take xx1,xx2,xx3,xx4,xx5; thus x = [xx1,xx2,xx3,xx4,xx5] by A3,A4,Def1; end; definition let X1,X2,X3,X4,X5; assume A1:X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{}; let x be Element of [:X1,X2,X3,X4,X5:]; func x`1 -> Element of X1 means :Def3: x = [x1,x2,x3,x4,x5] implies it = x1; existence proof consider xx1,xx2,xx3,xx4,xx5 such that A2: x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17; take xx1; thus thesis by A2,Th7; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5 such that A3: x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17; let y,z be Element of X1; assume x = [x1,x2,x3,x4,x5] implies y = x1; then A4: y = xx1 by A3; assume x = [x1,x2,x3,x4,x5] implies z = x1; hence thesis by A3,A4; end; func x`2 -> Element of X2 means :Def4: x = [x1,x2,x3,x4,x5] implies it = x2; existence proof consider xx1,xx2,xx3,xx4,xx5 such that A5: x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17; take xx2; thus thesis by A5,Th7; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5 such that A6: x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17; let y,z be Element of X2; assume x = [x1,x2,x3,x4,x5] implies y = x2; then A7: y = xx2 by A6; assume x = [x1,x2,x3,x4,x5] implies z = x2; hence thesis by A6,A7; end; func x`3 -> Element of X3 means :Def5: x = [x1,x2,x3,x4,x5] implies it = x3; existence proof consider xx1,xx2,xx3,xx4,xx5 such that A8: x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17; take xx3; thus thesis by A8,Th7; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5 such that A9: x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17; let y,z be Element of X3; assume x = [x1,x2,x3,x4,x5] implies y = x3; then A10: y = xx3 by A9; assume x = [x1,x2,x3,x4,x5] implies z = x3; hence thesis by A9,A10; end; func x`4 -> Element of X4 means :Def6: x = [x1,x2,x3,x4,x5] implies it = x4; existence proof consider xx1,xx2,xx3,xx4,xx5 such that A11: x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17; take xx4; thus thesis by A11,Th7; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5 such that A12: x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17; let y,z be Element of X4; assume x = [x1,x2,x3,x4,x5] implies y = x4; then A13: y = xx4 by A12; assume x = [x1,x2,x3,x4,x5] implies z = x4; hence thesis by A12,A13; end; func x`5 -> Element of X5 means :Def7: x = [x1,x2,x3,x4,x5] implies it = x5; existence proof consider xx1,xx2,xx3,xx4,xx5 such that A14: x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17; take xx5; thus thesis by A14,Th7; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5 such that A15: x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17; let y,z be Element of X5; assume x = [x1,x2,x3,x4,x5] implies y = x5; then A16: y = xx5 by A15; assume x = [x1,x2,x3,x4,x5] implies z = x5; hence thesis by A15,A16; end; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} implies for x being Element of [:X1,X2,X3,X4,X5:] for x1,x2,x3,x4,x5 st x = [x1,x2,x3,x4,x5] holds x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 & x`5 = x5 by Def3,Def4,Def5,Def6,Def7; theorem Th19: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} implies for x being Element of [:X1,X2,X3,X4,X5:] holds x = [x`1,x`2,x`3,x`4,x`5] proof assume A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{}; let x be Element of [:X1,X2,X3,X4,X5:]; consider xx1,xx2,xx3,xx4,xx5 such that A2: x = [xx1,xx2,xx3,xx4,xx5] by A1,Th17; thus x = [x`1,xx2,xx3,xx4,xx5] by A1,A2,Def3 .= [x`1,x`2,xx3,xx4,xx5] by A1,A2,Def4 .= [x`1,x`2,x`3,xx4,xx5] by A1,A2,Def5 .= [x`1,x`2,x`3,x`4,xx5] by A1,A2,Def6 .= [x`1,x`2,x`3,x`4,x`5] by A1,A2,Def7; end; theorem Th20: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} implies for x being Element of [:X1,X2,X3,X4,X5:] holds x`1 = (x qua set)`1`1`1`1 & x`2 = (x qua set)`1`1`1`2 & x`3 = (x qua set)`1`1`2 & x`4 = (x qua set)`1`2 & x`5 = (x qua set)`2 proof assume A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{}; let x be Element of [:X1,X2,X3,X4,X5:]; 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 Def1 .= (x qua set)`1`1`1`1 by A1,Th19; 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 Def1 .= (x qua set)`1`1`1`2 by A1,Th19; 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 Def1 .= (x qua set)`1`1`2 by A1,Th19; 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 Def1 .= (x qua set)`1`2 by A1,Th19; 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 Def1 .= (x qua set)`2 by A1,Th19; end; theorem X1 c= [:X1,X2,X3,X4,X5:] or X1 c= [:X2,X3,X4,X5,X1:] or X1 c= [:X3,X4,X5,X1,X2:] or X1 c= [:X4,X5,X1,X2,X3:] or X1 c= [:X5,X1,X2,X3,X4:] implies X1 = {} proof assume that A1: X1 c= [:X1,X2,X3,X4,X5:] or X1 c= [:X2,X3,X4,X5,X1:] or X1 c= [:X3,X4,X5,X1,X2:] or X1 c= [:X4,X5,X1,X2,X3:] or X1 c= [:X5,X1,X2,X3,X4:] and A2: X1 <> {}; [:X1,X2,X3,X4,X5:]<>{} or [:X2,X3,X4,X5,X1:]<>{} or [:X3,X4,X5,X1,X2:]<>{} or [:X4,X5,X1,X2,X3:]<>{} or [:X5,X1,X2,X3,X4:]<>{} by A1,A2,XBOOLE_1:3; then A3: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} by Th13; now per cases by A1; suppose A4: X1 c= [:X1,X2,X3,X4,X5:]; consider x such that A5: x in X1 and A6: for x1,x2,x3,x4,x5 st x1 in X1 or x2 in X1 holds x <> [x1,x2,x3,x4,x5] by A2,Th8; reconsider x as Element of [:X1,X2,X3,X4,X5:] by A4,A5; x = [x`1,x`2,x`3,x`4,x`5] & x`1 in X1 by A3,Th19; hence contradiction by A6; suppose X1 c= [:X2,X3,X4,X5,X1:]; then X1 c= [:[:X2,X3:],X4,X5,X1:] by Th12; hence thesis by A2,MCART_1:63; suppose X1 c= [:X3,X4,X5,X1,X2:]; then X1 c= [:[:X3,X4:],X5,X1,X2:] by Th12; hence thesis by A2,MCART_1:63; suppose X1 c= [:X4,X5,X1,X2,X3:]; then X1 c= [:[:X4,X5:],X1,X2,X3:] by Th12; hence thesis by A2,MCART_1:63; suppose A7: X1 c= [:X5,X1,X2,X3,X4:]; consider x such that A8: x in X1 and A9: for x1,x2,x3,x4,x5 st x1 in X1 or x2 in X1 holds x <> [x1,x2,x3,x4,x5] by A2,Th8; reconsider x as Element of [:X5,X1,X2,X3,X4:] by A7,A8; x = [x`1,x`2,x`3,x`4,x`5] & x`2 in X1 by A3,Th19; hence thesis by A9; end; hence contradiction; end; theorem [:X1,X2,X3,X4,X5:] meets [:Y1,Y2,Y3,Y4,Y5:] implies X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 proof A1: [:[:[:[:X1,X2:],X3:],X4:],X5:] = [:X1,X2,X3,X4,X5:] & [:[:[:[:Y1,Y2:],Y3:],Y4:],Y5:] = [:Y1,Y2,Y3,Y4,Y5:] by Th9; assume [:X1,X2,X3,X4,X5:] meets [:Y1,Y2,Y3,Y4,Y5:]; then [:[:[:X1,X2:],X3:],X4:] meets [:[:[:Y1,Y2:],Y3:],Y4:] & X5 meets Y5 by A1,ZFMISC_1:127; then [:[:X1,X2:],X3:] meets [:[:Y1,Y2:],Y3:] & X4 meets Y4 & X5 meets Y5 by ZFMISC_1:127; then [:X1,X2:] meets [:Y1,Y2:] & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 by ZFMISC_1:127; hence thesis by ZFMISC_1:127; end; theorem [:{x1},{x2},{x3},{x4},{x5}:] = { [x1,x2,x3,x4,x5] } proof thus [:{x1},{x2},{x3},{x4},{x5}:] = [:[:{x1},{x2}:],{x3},{x4},{x5}:] by Th12 .= [:{[x1,x2]}, {x3},{x4},{x5}:] by ZFMISC_1:35 .= { [[x1,x2], x3, x4, x5]} by MCART_1:65 .= { [x1,x2,x3,x4,x5] } by Th6; 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; :: 5 - Tuples reserve x for Element of [:X1,X2,X3,X4,X5:]; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} implies for x1,x2,x3,x4,x5 st x = [x1,x2,x3,x4,x5] holds x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 & x`5 = x5 by Def3,Def4,Def5 ,Def6,Def7; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & (for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y1 = xx1) implies y1 =x`1 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} and A2: for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y1 = xx1; x = [x`1,x`2,x`3,x`4,x`5] by A1,Th19; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & (for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y2 = xx2) implies y2 =x`2 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} and A2: for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y2 = xx2; x = [x`1,x`2,x`3,x`4,x`5] by A1,Th19; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & (for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y3 = xx3) implies y3 =x`3 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} and A2: for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y3 = xx3; x = [x`1,x`2,x`3,x`4,x`5] by A1,Th19; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & (for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y4 = xx4) implies y4 =x`4 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} and A2: for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y4 = xx4; x = [x`1,x`2,x`3,x`4,x`5] by A1,Th19; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & (for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y5 = xx5) implies y5 =x`5 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} and A2: for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y5 = xx5; x = [x`1,x`2,x`3,x`4,x`5] by A1,Th19; hence thesis by A2; end; theorem y in [: X1,X2,X3,X4,X5 :] implies ex x1,x2,x3,x4,x5 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & y = [x1,x2,x3,x4,x5] proof assume y in [: X1,X2,X3,X4,X5 :]; then y in [:[:X1,X2,X3,X4:],X5:] by Def2; then consider x1234, x5 being set such that A1: x1234 in [:X1,X2,X3,X4:] and A2: x5 in X5 and A3: y = [x1234,x5] by ZFMISC_1:def 2; consider x1, x2, x3, x4 such that A4: x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x1234 = [x1,x2,x3,x4] by A1,MCART_1:83; y = [x1,x2,x3,x4,x5] by A3,A4,Def1; hence thesis by A2,A4; end; theorem [x1,x2,x3,x4,x5] in [: X1,X2,X3,X4,X5 :] iff x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 proof A1: [:X1,X2,X3,X4,X5:] = [:[:X1,X2:],X3,X4,X5:] by Th12; A2: [x1,x2,x3,x4,x5] = [[x1,x2],x3,x4,x5] by Th6; [x1,x2] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:106; hence thesis by A1,A2,MCART_1:84; end; theorem (for y holds y in Z iff ex x1,x2,x3,x4,x5 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & y = [x1,x2,x3,x4,x5]) implies Z = [: X1,X2,X3,X4,X5 :] proof assume A1: for y holds y in Z iff ex x1,x2,x3,x4,x5 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & y = [x1,x2,x3,x4,x5]; now let y; thus y in Z implies y in [:[:X1,X2,X3,X4:],X5:] proof assume y in Z; then consider x1,x2,x3,x4,x5 such that A2: x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & y = [x1,x2,x3,x4,x5] by A1; A3: y = [[x1,x2,x3,x4],x5] by A2,Def1; [x1,x2,x3,x4] in [:X1,X2,X3,X4:] & x5 in X5 by A2,MCART_1:84; hence y in [:[:X1,X2,X3,X4:],X5:] by A3,ZFMISC_1:def 2; end; assume y in [:[:X1,X2,X3,X4:],X5:]; then consider x1234,x5 being set such that A4: x1234 in [:X1,X2,X3,X4:] and A5: x5 in X5 and A6: y = [x1234,x5] by ZFMISC_1:def 2; consider x1,x2,x3,x4 such that A7: x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x1234 = [x1,x2,x3,x4] by A4,MCART_1:83; y = [x1,x2,x3,x4,x5] by A6,A7,Def1; hence y in Z by A1,A5,A7; end; then Z = [:[:X1,X2,X3,X4:],X5:] by TARSKI:2; hence Z = [: X1,X2,X3,X4,X5 :] by Def2; end; theorem Th33: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} & Y5<>{} implies for x being Element of [:X1,X2,X3,X4,X5:], y being Element of [:Y1,Y2,Y3,Y4,Y5:] holds x = y implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3 & x`4 = y`4 & x`5 = y`5 proof assume that A1: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} and A2: Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {} & Y5 <> {}; let x be Element of [:X1,X2,X3,X4,X5:]; let y be Element of [:Y1,Y2,Y3,Y4,Y5:]; assume A3: x = y; thus x`1 = (x qua set)`1`1`1`1 by A1,Th20 .= y`1 by A2,A3,Th20; thus x`2 = (x qua set)`1`1`1`2 by A1,Th20 .= y`2 by A2,A3,Th20; thus x`3 = (x qua set)`1`1`2 by A1,Th20 .= y`3 by A2,A3,Th20; thus x`4 = (x qua set)`1`2 by A1,Th20 .= y`4 by A2,A3,Th20; thus x`5 = (x qua set)`2 by A1,Th20 .= y`5 by A2,A3,Th20; end; theorem for x being Element of [:X1,X2,X3,X4,X5:] st x in [:A1,A2,A3,A4,A5:] holds x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4 & x`5 in A5 proof let x be Element of [:X1,X2,X3,X4,X5:]; assume A1: x in [:A1,A2,A3,A4,A5:]; then A2: A1 <> {} & A2 <> {} & A3 <> {} & A4 <> {} & A5 <> {} by Th13; reconsider y = x as Element of [:A1,A2,A3,A4,A5:] by A1; y`1 in A1 & y`2 in A2 & y`3 in A3 & y`4 in A4 & y`5 in A5 by A2; hence x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4 & x`5 in A5 by Th33; end; theorem Th35: X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 implies [:X1,X2,X3,X4,X5:] c= [:Y1,Y2,Y3,Y4,Y5:] proof assume X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4; then A1: [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:] by MCART_1:88; A2: [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3,X4:],X5:] & [:Y1,Y2,Y3,Y4,Y5:] = [:[:Y1,Y2,Y3,Y4:],Y5:] by Def2; assume X5 c= Y5; hence thesis by A1,A2,ZFMISC_1:119; end; definition let X1,X2,X3,X4,X5,A1,A2,A3,A4,A5; redefine func [:A1,A2,A3,A4,A5:] -> Subset of [:X1,X2,X3,X4,X5:]; coherence by Th35; end; theorem X1 <> {} & X2 <> {} implies for xx being Element of [:X1,X2:] ex xx1 being (Element of X1), xx2 being Element of X2 st xx = [xx1,xx2] by Lm1; theorem X1 <> {} & X2 <> {} & X3 <> {} implies for xx being Element of [:X1,X2,X3:] ex xx1,xx2,xx3 st xx = [xx1,xx2,xx3] by Lm2; theorem X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} implies for xx being Element of [:X1,X2,X3,X4:] ex xx1,xx2,xx3,xx4 st xx = [xx1,xx2,xx3,xx4] by Lm3;

Back to top