### The Mizar article:

### Tuples, Projections and Cartesian Products

**by****Andrzej Trybulec**

- Received March 30, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: MCART_1
- [ MML identifier index ]

environ vocabulary BOOLE, TARSKI, MCART_1; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1; constructors TARSKI, ENUMSET1, SUBSET_1, XBOOLE_0; clusters XBOOLE_0, ZFMISC_1; requirements SUBSET, BOOLE; theorems TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, ORDINAL1, XBOOLE_1; schemes XBOOLE_0; begin reserve v,x,x1,x2,x3,x4,y,y1,y2,y3,y4,z,z1,z2 for set, X,X1,X2,X3,X4,Y,Y1,Y2,Y3,Y4,Y5,Z,Z1,Z2,Z3,Z4,Z5 for set; :: :: Regularity :: :: We start with some auxiliary theorems related to the regularity axiom. :: We need them to prove theorems below. Nevertheless they are :: marked as theorems because they seem to be of general interest. theorem Th1: X <> {} implies ex Y st Y in X & Y misses X proof assume A1: X <> {}; consider x being Element of X; x in X by A1; then consider Y such that A2: Y in X & not ex x st x in X & x in Y by TARSKI:7; take Y; thus thesis by A2,XBOOLE_0:3; end; theorem Th2: X <> {} implies ex Y st Y in X & for Y1 st Y1 in Y holds Y1 misses X proof defpred P[set] means $1 meets X; consider Z such that A1: for Y holds Y in Z iff Y in union X & P[Y] from Separation; assume X <> {}; then X \/ Z <> {} by XBOOLE_1:15; then consider Y such that A2: Y in X \/ Z and A3: Y misses X \/ Z by Th1; assume A4: not thesis; now assume A5: Y in X; then consider Y1 such that A6: Y1 in Y & not Y1 misses X by A4; Y1 in union X & Y1 meets X by A5,A6,TARSKI:def 4; then Y1 in Z by A1; then Y1 in X \/ Z by XBOOLE_0:def 2; hence contradiction by A3,A6,XBOOLE_0:3; end; then Y in Z by A2,XBOOLE_0:def 2; then Y meets X by A1; hence contradiction by A3,XBOOLE_1:70; end; theorem X <> {} implies ex Y st Y in X & for Y1,Y2 st Y1 in Y2 & Y2 in Y holds Y1 misses X proof defpred P[set] means ex Y1 st Y1 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 $1 meets X; consider Z2 such that A2: for Y holds Y in Z2 iff Y in union union X & Q[Y] from Separation; assume X <> {}; then X \/ Z1 <> {} by XBOOLE_1:15; then X \/ Z1 \/ Z2 <> {} by XBOOLE_1:15; then consider Y such that A3: Y in X \/ Z1 \/ Z2 and A4: Y misses X \/ Z1 \/ Z2 by Th1; A5: Y in X \/ (Z1 \/ Z2) by A3,XBOOLE_1:4; assume A6: not thesis; now assume A7: Y in X; then consider Y1,Y2 such that A8: Y1 in Y2 & Y2 in Y & not Y1 misses X by A6; Y2 in union X & Y1 meets X by A7,A8,TARSKI:def 4; then Y2 in Z1 by A1,A8; then Y2 in X \/ Z1 by XBOOLE_0:def 2; then Y2 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; hence contradiction by A4,A8,XBOOLE_0:3; end; then A9: Y in Z1 \/ Z2 by A5,XBOOLE_0:def 2; now assume A10: Y in Z1; then consider Y1 such that A11: Y1 in Y & Y1 meets X by A1; Y in union X by A1,A10; then Y1 in union union X by A11,TARSKI:def 4; then Y1 in Z2 by A2,A11; then Y1 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; hence contradiction by A4,A11,XBOOLE_0:3; end; then Y in Z2 by A9,XBOOLE_0:def 2; then Y meets X by A2; then Y meets X \/ Z1 by XBOOLE_1:70; hence contradiction by A4,XBOOLE_1:70; end; theorem Th4: X <> {} implies ex Y st Y in X & for Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in Y holds Y1 misses X proof defpred P[set] means ex Y1,Y2 st Y1 in Y2 & Y2 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 st Y1 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 $1 meets X; consider Z3 such that A3: for Y holds Y in Z3 iff Y in union union union X & R[Y] from Separation; set V = X \/ Z1 \/ Z2 \/ Z3; A4: V = X \/ (Z1 \/ Z2) \/ Z3 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3) by XBOOLE_1:4; assume X <> {}; then V <> {} by A4,XBOOLE_1:15; then consider Y such that A5: Y in X \/ Z1 \/ Z2 \/ Z3 and A6: Y misses X \/ Z1 \/ Z2 \/ Z3 by Th1; assume A7: not thesis; now assume A8: Y in X; then consider Y1,Y2,Y3 such that A9: Y1 in Y2 & Y2 in Y3 & Y3 in Y & not Y1 misses X by A7; Y3 in union X & Y1 meets X by A8,A9,TARSKI:def 4; then Y3 in Z1 by A1,A9; then Y3 in X \/ Z1 by XBOOLE_0:def 2; then Y3 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then Y3 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; hence contradiction by A6,A9,XBOOLE_0:3; end; then Y in Z1 \/ Z2 \/ Z3 by A4,A5,XBOOLE_0:def 2; then A10: Y in Z1 \/ (Z2 \/ Z3) by XBOOLE_1:4; now assume A11: Y in Z1; then consider Y1,Y2 such that A12: Y1 in Y2 & Y2 in Y & Y1 meets X by A1; Y in union X by A1,A11; then Y2 in union union X by A12,TARSKI:def 4; then Y2 in Z2 by A2,A12; then Y2 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 by A12,XBOOLE_0:3; hence contradiction by A6,XBOOLE_1:70; end; then A13: Y in Z2 \/ Z3 by A10,XBOOLE_0:def 2; now assume A14: Y in Z2; then consider Y1 such that A15: Y1 in Y & Y1 meets X by A2; Y in union union X by A2,A14; then Y1 in union union union X by A15,TARSKI:def 4; then Y1 in Z3 by A3,A15; then Y1 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; hence contradiction by A6,A15,XBOOLE_0:3; end; then Y in Z3 by A13,XBOOLE_0:def 2; then Y meets X by A3; hence contradiction by A4,A6,XBOOLE_1:70; end; theorem X <> {} implies ex Y st Y in X & for Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y holds Y1 misses X proof defpred P[set] means ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 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 st Y1 in Y2 & Y2 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 st Y1 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 $1 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; A5: X \/ Z1 \/ Z2 \/ Z3 \/ Z4 = X \/ (Z1 \/ Z2) \/ Z3 \/ Z4 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3) \/ Z4 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4) by XBOOLE_1:4; assume X <> {}; then X \/ Z1 \/ Z2 \/ Z3 \/ Z4 <> {} by A5,XBOOLE_1:15; then consider Y such that A6: Y in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 and A7: Y misses X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by Th1; assume A8: not thesis; now assume A9: Y in X; then consider Y1,Y2,Y3,Y4 such that A10: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & not Y1 misses X by A8; Y4 in union X & Y1 meets X by A9,A10,TARSKI:def 4; then Y4 in Z1 by A1,A10; then Y4 in X \/ Z1 by XBOOLE_0:def 2; then Y4 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; 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; hence contradiction by A7,A10,XBOOLE_0:3; end; then Y in Z1 \/ Z2 \/ Z3 \/ Z4 by A5,A6,XBOOLE_0:def 2; then Y in Z1 \/ (Z2 \/ Z3) \/ Z4 by XBOOLE_1:4; then A11: Y in Z1 \/ (Z2 \/ Z3 \/ Z4) by XBOOLE_1:4; now assume A12: Y in Z1; then consider Y1,Y2,Y3 such that A13: Y1 in Y2 & Y2 in Y3 & Y3 in Y & Y1 meets X by A1; Y in union X by A1,A12; then Y3 in union union X by A13,TARSKI:def 4; then Y3 in Z2 by A2,A13; then Y3 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 by A13,XBOOLE_0:3; then Y meets X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_1:70; hence contradiction by A7,XBOOLE_1:70; end; then Y in Z2 \/ Z3 \/ Z4 by A11,XBOOLE_0:def 2; then A14: Y in Z2 \/ (Z3 \/ Z4) by XBOOLE_1:4; now assume A15: Y in Z2; then consider Y1,Y2 such that A16: Y1 in Y2 & Y2 in Y & Y1 meets X by A2; Y in union union X by A2,A15; then Y2 in union union union X by A16,TARSKI:def 4; then Y2 in Z3 by A3,A16; then Y2 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 \/ Z3 by A16,XBOOLE_0:3; hence contradiction by A7,XBOOLE_1:70; end; then A17: Y in Z3 \/ Z4 by A14,XBOOLE_0:def 2; now assume A18: Y in Z3; then consider Y1 such that A19: Y1 in Y & Y1 meets X by A3; Y in union union union X by A3,A18; then Y1 in union union union union X by A19,TARSKI:def 4; then Y1 in Z4 by A4,A19; then Y1 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; hence contradiction by A7,A19,XBOOLE_0:3; end; then Y in Z4 by A17,XBOOLE_0:def 2; then Y meets X by A4; hence contradiction by A5,A7,XBOOLE_1:70; end; theorem Th6: X <> {} implies ex Y st Y in X & for Y1,Y2,Y3,Y4,Y5 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y holds Y1 misses X proof defpred P[set] means ex Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 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 st Y1 in Y2 & Y2 in Y3 & Y3 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 st Y1 in Y2 & Y2 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 st Y1 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 $1 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; set V = X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5; A6: V = X \/ (Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) by XBOOLE_1:4; assume X <> {}; then V <> {} by A6,XBOOLE_1:15; then consider Y such that A7: Y in V and A8: Y misses V by Th1; assume A9: not thesis; now assume A10: Y in X; then consider Y1,Y2,Y3,Y4,Y5 such that A11: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y & not Y1 misses X by A9; Y5 in union X & Y1 meets X by A10,A11,TARSKI:def 4; then Y5 in Z1 by A1,A11; then Y5 in X \/ Z1 by XBOOLE_0:def 2; then Y5 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then Y5 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 \/ Z3 by A11,XBOOLE_0:3; then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_1:70; hence contradiction by A8,XBOOLE_1:70; end; then Y in Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by A6,A7,XBOOLE_0:def 2; then Y in Z1 \/ (Z2 \/ Z3) \/ Z4 \/ Z5 by XBOOLE_1:4; then Y in Z1 \/ (Z2 \/ Z3 \/ Z4) \/ Z5 by XBOOLE_1:4; then A12: Y in Z1 \/ (Z2 \/ Z3 \/ Z4 \/ Z5) by XBOOLE_1:4; now assume A13: Y in Z1; then consider Y1,Y2,Y3,Y4 such that A14: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & Y1 meets X by A1; Y in union X by A1,A13; then Y4 in union union X by A14,TARSKI:def 4; then Y4 in Z2 by A2,A14; then Y4 in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 by A14,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; hence contradiction by A8,XBOOLE_1:70; end; then Y in Z2 \/ Z3 \/ Z4 \/ Z5 by A12,XBOOLE_0:def 2; then Y in Z2 \/ (Z3 \/ Z4) \/ Z5 by XBOOLE_1:4; then A15: Y in Z2 \/ (Z3 \/ Z4 \/ Z5) by XBOOLE_1:4; now assume A16: Y in Z2; then consider Y1,Y2,Y3 such that A17: Y1 in Y2 & Y2 in Y3 & Y3 in Y & Y1 meets X by A2; Y in union union X by A2,A16; then Y3 in union union union X by A17,TARSKI:def 4; then Y3 in Z3 by A3,A17; then Y3 in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; then Y3 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then Y3 in V by XBOOLE_0:def 2; hence contradiction by A8,A17,XBOOLE_0:3; end; then Y in Z3 \/ Z4 \/ Z5 by A15,XBOOLE_0:def 2; then A18: Y in Z3 \/ (Z4 \/ Z5) by XBOOLE_1:4; now assume A19: Y in Z3; then consider Y1,Y2 such that A20: Y1 in Y2 & Y2 in Y & Y1 meets X by A3; Y in union union union X by A3,A19; then Y2 in union union union union X by A20,TARSKI:def 4; then Y2 in Z4 by A4,A20; then Y2 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then Y2 in V by XBOOLE_0:def 2; hence contradiction by A8,A20,XBOOLE_0:3; end; then A21: Y in Z4 \/ Z5 by A18,XBOOLE_0:def 2; now assume A22: Y in Z4; then consider Y1 such that A23: Y1 in Y & Y1 meets X by A4; Y in union union union union X by A4,A22; then Y1 in union union union union union X by A23,TARSKI:def 4; then Y1 in Z5 by A5,A23; then Y1 in V by XBOOLE_0:def 2; hence contradiction by A8,A23,XBOOLE_0:3; end; then Y in Z5 by A21,XBOOLE_0:def 2; then Y meets X by A5; hence contradiction by A6,A8,XBOOLE_1:70; end; :: :: Ordered pairs :: :: Now we introduce the projections of ordered pairs (functions that assign :: to an ordered pair its first and its second element). The definitions :: are permissive, function are defined for an arbitrary object. If it is not :: an ordered pair, they are of course meaningless. definition let x; given x1,x2 being set such that A1: x = [x1,x2]; func x`1 means :Def1: x = [y1,y2] implies it = y1; existence proof take x1; thus thesis by A1,ZFMISC_1:33; end; uniqueness proof let z1,z2; assume (for y1,y2 st x = [y1,y2] holds z1 = y1) & (for y1,y2 st x = [y1,y2] holds z2 = y1); then z1 = x1 & z2 = x1 by A1; hence z1 = z2; end; func x`2 means :Def2: x = [y1,y2] implies it = y2; existence proof take x2; thus thesis by A1,ZFMISC_1:33; end; uniqueness proof let z1,z2; assume (for y1,y2 st x = [y1,y2] holds z1 = y2) & (for y1,y2 st x = [y1,y2] holds z2 = y2); then z1 = x2 & z2 = x2 by A1; hence z1 = z2; end; end; theorem [x,y]`1=x & [x,y]`2=y by Def1,Def2; theorem Th8: (ex x,y st z=[x,y]) implies [z`1,z`2] =z proof given x,y such that A1: z=[x,y]; z`1=x & z`2=y by A1,Def1,Def2; hence thesis by A1; end; theorem X <> {} implies ex v st v in X & not ex x,y st (x in X or y in X) & v = [x,y] proof assume X <> {}; then consider Y such that A1: Y in X and A2: not ex Y1 st Y1 in Y & not Y1 misses X by Th2; take v = Y; thus v in X by A1; given x,y such that A3: x in X or y in X and A4: v = [x,y]; x in { x,y } & y in { x,y } by TARSKI:def 2; then A5: not { x,y } misses X by A3,XBOOLE_0:3; Y = { {x,y}, {x} } by A4,TARSKI:def 5; then { x,y } in Y by TARSKI:def 2; hence contradiction by A2,A5; end; :: Now we prove theorems describing relationships between projections :: of ordered pairs and Cartesian products of two sets. theorem Th10: z in [:X,Y:] implies z`1 in X & z`2 in Y proof assume z in [:X,Y:]; then ex x,y st x in X & y in Y & z=[x,y] by ZFMISC_1:def 2; hence z`1 in X & z`2 in Y by Def1,Def2; end; theorem (ex x,y st z=[x,y]) & z`1 in X & z`2 in Y implies z in [:X,Y:] proof assume ex x,y st z=[x,y]; then [z`1,z`2]=z by Th8; hence thesis by ZFMISC_1:def 2; end; theorem z in [:{x},Y:] implies z`1=x & z`2 in Y proof assume z in [:{x},Y:]; then z`1 in {x} & z`2 in Y by Th10; hence thesis by TARSKI:def 1; end; theorem z in [:X,{y}:] implies z`1 in X & z`2 = y proof assume z in [:X,{y}:]; then z`1 in X & z`2 in {y} by Th10; hence thesis by TARSKI:def 1; end; theorem z in [:{x},{y}:] implies z`1 = x & z`2 = y proof assume z in [:{x},{y}:]; then z`1 in {x} & z`2 in {y} by Th10; hence thesis by TARSKI:def 1; end; theorem z in [:{x1,x2},Y:] implies (z`1=x1 or z`1=x2) & z`2 in Y proof assume z in [:{x1,x2},Y:]; then z`1 in {x1,x2} & z`2 in Y by Th10; hence thesis by TARSKI:def 2; end; theorem z in [:X,{y1,y2}:] implies z`1 in X & (z`2 = y1 or z`2 = y2) proof assume z in [:X,{y1,y2}:]; then z`1 in X & z`2 in {y1,y2} by Th10; hence thesis by TARSKI:def 2; end; theorem z in [:{x1,x2},{y}:] implies (z`1=x1 or z`1=x2) & z`2 = y proof assume z in [:{x1,x2},{y}:]; then z`1 in {x1,x2} & z`2 in {y} by Th10; hence thesis by TARSKI:def 1,def 2; end; theorem z in [:{x},{y1,y2}:] implies z`1 = x & (z`2 = y1 or z`2 = y2) proof assume z in [:{x},{y1,y2}:]; then z`1 in {x} & z`2 in {y1,y2} by Th10; hence thesis by TARSKI:def 1,def 2; end; theorem z in [:{x1,x2},{y1,y2}:] implies (z`1 = x1 or z`1 = x2) & (z`2 = y1 or z`2 = y2) proof assume z in [:{x1,x2},{y1,y2}:]; then z`1 in {x1,x2} & z`2 in {y1,y2} by Th10; hence thesis by TARSKI:def 2; end; theorem Th20: (ex y,z st x = [y,z]) implies x <> x`1 & x <> x`2 proof given y,z such that A1: x = [y,z]; A2: x = {{y,z},{y}} by A1,TARSKI:def 5; now assume y = x; then {{y,z},{y}} in {y} & {y} in {{y,z},{y}} by A2,TARSKI:def 1,def 2; hence contradiction; end; hence x <> x`1 by A1,Def1; now assume z = x; then {{y,z},{y}} in {y,z} & {y,z} in {{y,z},{y}} by A2,TARSKI:def 2; hence contradiction; end; hence thesis by A1,Def2; end; :: Some of theorems proved above may be simplified , if we state them :: for elements of Cartesian product rather than for arbitrary objects. canceled 2; theorem Th23: x in [:X,Y:] implies x = [x`1,x`2] proof assume x in [:X,Y:]; then ex x1,x2 st x=[x1,x2] by ZFMISC_1:102; hence x = [x`1,x`2] by Th8; end; theorem Th24: X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x = [x`1,x`2] proof assume X <> {} & Y <> {}; then A1: [:X,Y:] <> {} by ZFMISC_1:113; let x be Element of [:X,Y:]; thus thesis by A1,Th23; end; 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,Th10; reconsider xx2 = x`2 as Element of X2 by A2,Th10; take xx1,xx2; thus x = [xx1,xx2] by A1,Th24; end; theorem Th25: [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]} proof thus [:{x1,x2},{y1,y2}:] = [:{x1},{y1,y2}:] \/ [:{x2},{y1,y2}:] by ZFMISC_1:132 .= {[x1,y1],[x1,y2]} \/ [:{x2},{y1,y2}:] by ZFMISC_1:36 .= {[x1,y1],[x1,y2]} \/ {[x2,y1],[x2,y2]} by ZFMISC_1:36 .= {[x1,y1],[x1,y2],[x2,y1],[x2,y2]} by ENUMSET1:45; end; theorem Th26: X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x <> x`1 & x <> x`2 proof assume A1: X <> {} & Y <> {}; let x be Element of [:X,Y:]; x = [x`1,x`2] by A1,Th24; hence thesis by Th20; end; :: :: Triples :: definition let x1,x2,x3; func [x1,x2,x3] equals :Def3: [[x1,x2],x3]; correctness; end; canceled; theorem Th28: [x1,x2,x3] = [y1,y2,y3] implies x1 = y1 & x2 = y2 & x3 = y3 proof assume [x1,x2,x3] = [y1,y2,y3]; then [[x1,x2],x3] = [y1,y2,y3] by Def3 .= [[y1,y2],y3] by Def3; then [x1,x2] = [y1,y2] & x3 = y3 by ZFMISC_1:33; hence thesis by ZFMISC_1:33; end; theorem Th29: X <> {} implies ex v st v in X & not ex x,y,z st (x in X or y in X) & v = [x,y,z] proof assume X <> {}; then consider Y such that A1: Y in X and A2: not ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in Y & not Y1 misses X by Th4; take v = Y; thus v in X by A1; given x,y,z such that A3: x in X or y in X and A4: v = [x,y,z]; set Y1 = { x,y }, Y2 = { Y1,{x} }, Y3 = { Y2,z }; x in Y1 & y in Y1 by TARSKI:def 2; then A5: not Y1 misses X by A3,XBOOLE_0:3; Y = [[x,y],z] by A4,Def3 .= [ Y2,z ] by TARSKI:def 5 .= { Y3,{ Y2 } } by TARSKI:def 5; then Y1 in Y2 & Y2 in Y3 & Y3 in Y by TARSKI:def 2; hence contradiction by A2,A5; end; :: :: Quadruples :: definition let x1,x2,x3,x4; func [x1,x2,x3,x4] equals :Def4: [[x1,x2,x3],x4]; correctness; end; canceled; theorem Th31: [x1,x2,x3,x4] = [[[x1,x2],x3],x4] proof thus [x1,x2,x3,x4] = [[x1,x2,x3],x4] by Def4 .= [[[x1,x2],x3],x4] by Def3; end; theorem Th32: [x1,x2,x3,x4] = [[x1,x2],x3,x4] proof thus [x1,x2,x3,x4] = [[[x1,x2],x3],x4] by Th31 .= [[x1,x2],x3,x4] by Def3; end; theorem Th33: [x1,x2,x3,x4] = [y1,y2,y3,y4] implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 proof assume [x1,x2,x3,x4] = [y1,y2,y3,y4]; then [[x1,x2,x3],x4] = [y1,y2,y3,y4] by Def4 .= [[y1,y2,y3],y4] by Def4; then [x1,x2,x3] = [y1,y2,y3] & x4 = y4 by ZFMISC_1:33; hence thesis by Th28; end; theorem Th34: X <> {} implies ex v st v in X & not ex x1,x2,x3,x4 st (x1 in X or x2 in X) & v = [x1,x2,x3,x4] proof assume X <> {}; then consider Y such that A1: Y in X and A2: for Y1,Y2,Y3,Y4,Y5 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y holds Y1 misses X by Th6; take v = Y; thus v in X by A1; given x1,x2,x3,x4 such that A3: x1 in X or x2 in X and A4: v = [x1,x2,x3,x4]; set Y1 = { x1,x2 }, Y2 = { Y1,{x1} }, Y3 = { Y2,x3 }, Y4 = { Y3, {Y2}}, Y5 = { Y4,x4 }; 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] by A4,Th31 .= [[ Y2,x3],x4 ] by TARSKI:def 5 .= [ Y4,x4 ] by TARSKI:def 5 .= { Y5,{ Y4 } } by TARSKI:def 5; then Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y by TARSKI:def 2; hence contradiction by A2,A5; end; :: :: Cartesian products of three sets :: theorem Th35: X1 <> {} & X2 <> {} & X3 <> {} iff [:X1,X2,X3:] <> {} proof A1: [:[:X1,X2:],X3:] = [:X1,X2,X3:] by ZFMISC_1:def 3; X1 <> {} & X2 <> {} iff [:X1,X2:] <> {} by ZFMISC_1:113; hence thesis by A1,ZFMISC_1:113; end; reserve xx1 for Element of X1, xx2 for Element of X2, xx3 for Element of X3; theorem Th36: X1<>{} & X2<>{} & X3<>{} implies ( [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies X1=Y1 & X2=Y2 & X3=Y3) proof A1: [:X1,X2,X3:] = [:[:X1,X2:],X3:] by ZFMISC_1:def 3; assume A2: X1<>{} & X2<>{}; then A3: [:X1,X2:] <> {} by ZFMISC_1:113; assume A4: X3<>{}; assume [:X1,X2,X3:] = [:Y1,Y2,Y3:]; then [:[:X1,X2:],X3:] = [:[:Y1,Y2:],Y3:] by A1,ZFMISC_1:def 3; then [:X1,X2:] = [:Y1,Y2:] & X3 = Y3 by A3,A4,ZFMISC_1:134; hence thesis by A2,ZFMISC_1:134; end; theorem [:X1,X2,X3:]<>{} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies X1=Y1 & X2=Y2 & X3=Y3 proof assume [:X1,X2,X3:]<>{}; then X1<>{} & X2<>{} & X3<>{} by Th35; hence thesis by Th36; end; theorem [:X,X,X:] = [:Y,Y,Y:] implies X = Y proof assume [:X,X,X:] = [:Y,Y,Y:]; then X<>{} or Y<>{} implies thesis by Th36; hence X = Y; 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,Def3; end; theorem Th39:[:{x1},{x2},{x3}:] = { [x1,x2,x3] } proof thus [:{x1},{x2},{x3}:] = [:[:{x1},{x2}:],{x3}:] by ZFMISC_1:def 3 .= [:{[x1,x2]},{x3}:] by ZFMISC_1:35 .= {[[x1,x2],x3]} by ZFMISC_1:35 .= { [x1,x2,x3] }by Def3; end; theorem [:{x1,y1},{x2},{x3}:] = { [x1,x2,x3],[y1,x2,x3] } proof thus [:{x1,y1},{x2},{x3}:] = [:[:{x1,y1},{x2}:],{x3}:] by ZFMISC_1:def 3 .= [:{[x1,x2],[y1,x2]},{x3}:] by ZFMISC_1:36 .= {[[x1,x2],x3],[[y1,x2],x3]} by ZFMISC_1:36 .= { [x1,x2,x3],[[y1,x2],x3] } by Def3 .= { [x1,x2,x3],[y1,x2,x3] } by Def3; end; theorem [:{x1},{x2,y2},{x3}:] = { [x1,x2,x3],[x1,y2,x3] } proof thus [:{x1},{x2,y2},{x3}:] = [:[:{x1},{x2,y2}:],{x3}:] by ZFMISC_1:def 3 .= [:{[x1,x2],[x1,y2]},{x3}:] by ZFMISC_1:36 .= {[[x1,x2],x3],[[x1,y2],x3]} by ZFMISC_1:36 .= { [x1,x2,x3],[[x1,y2],x3] } by Def3 .= { [x1,x2,x3],[x1,y2,x3] } by Def3; end; theorem [:{x1},{x2},{x3,y3}:] = { [x1,x2,x3],[x1,x2,y3] } proof thus [:{x1},{x2},{x3,y3}:] = [:[:{x1},{x2}:],{x3,y3}:] by ZFMISC_1:def 3 .= [:{[x1,x2]},{x3,y3}:] by ZFMISC_1:35 .= {[[x1,x2],x3],[[x1,x2],y3]} by ZFMISC_1:36 .= { [x1,x2,x3],[[x1,x2],y3] } by Def3 .= { [x1,x2,x3],[x1,x2,y3] } by Def3; end; theorem [:{x1,y1},{x2,y2},{x3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3] } proof thus [:{x1,y1},{x2,y2},{x3}:] = [:[:{x1,y1},{x2,y2}:],{x3}:] by ZFMISC_1:def 3 .= [:{[x1,x2],[x1,y2],[y1,x2],[y1,y2]},{x3}:] by Th25 .= [:{[x1,x2],[x1,y2]} \/ {[y1,x2],[y1,y2]},{x3}:] by ENUMSET1:45 .= [:{[x1,x2],[x1,y2]},{x3}:] \/ [:{[y1,x2],[y1,y2]},{x3}:] by ZFMISC_1:120 .= { [[x1,x2],x3],[[x1,y2],x3]} \/ [:{[y1,x2],[y1,y2]},{x3}:] by ZFMISC_1:36 .= { [[x1,x2],x3],[[x1,y2],x3]} \/ {[[y1,x2],x3],[[y1,y2],x3] } by ZFMISC_1:36 .= { [[x1,x2],x3],[[x1,y2],x3],[[y1,x2],x3],[[y1,y2],x3] } by ENUMSET1:45 .= { [x1,x2,x3],[[x1,y2],x3],[[y1,x2],x3],[[y1,y2],x3] } by Def3 .= { [x1,x2,x3],[x1,y2,x3],[[y1,x2],x3],[[y1,y2],x3] } by Def3 .= { [x1,x2,x3],[x1,y2,x3],[y1,x2,x3],[[y1,y2],x3] } by Def3 .= { [x1,x2,x3],[x1,y2,x3],[y1,x2,x3],[y1,y2,x3] } by Def3 .= { [x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3] } by ENUMSET1:104; end; theorem [:{x1,y1},{x2},{x3,y3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3] } proof thus [:{x1,y1},{x2},{x3,y3}:] = [:[:{x1,y1},{x2}:],{x3,y3}:] by ZFMISC_1:def 3 .= [:{[x1,x2],[y1,x2]},{x3,y3}:] by ZFMISC_1:36 .= { [[x1,x2],x3],[[x1,x2],y3],[[y1,x2],x3],[[y1,x2],y3] } by Th25 .= { [[x1,x2],x3],[[y1,x2],x3],[[x1,x2],y3],[[y1,x2],y3] } by ENUMSET1:104 .= { [x1,x2,x3],[[y1,x2],x3],[[x1,x2],y3],[[y1,x2],y3] } by Def3 .= { [x1,x2,x3],[y1,x2,x3],[[x1,x2],y3],[[y1,x2],y3] } by Def3 .= { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[[y1,x2],y3] } by Def3 .= { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3] } by Def3; end; theorem [:{x1},{x2,y2},{x3,y3}:] = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3] } proof thus [:{x1},{x2,y2},{x3,y3}:] = [:[:{x1},{x2,y2}:],{x3,y3}:] by ZFMISC_1:def 3 .= [:{[x1,x2],[x1,y2]},{x3,y3}:] by ZFMISC_1:36 .= { [[x1,x2],x3],[[x1,x2],y3],[[x1,y2],x3],[[x1,y2],y3] } by Th25 .= { [[x1,x2],x3],[[x1,y2],x3],[[x1,x2],y3],[[x1,y2],y3] } by ENUMSET1:104 .= { [x1,x2,x3],[[x1,y2],x3],[[x1,x2],y3],[[x1,y2],y3] } by Def3 .= { [x1,x2,x3],[x1,y2,x3],[[x1,x2],y3],[[x1,y2],y3] } by Def3 .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[[x1,y2],y3] } by Def3 .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3] } by Def3; end; theorem [:{x1,y1},{x2,y2},{x3,y3}:] = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3], [y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3] } proof A1: [:{[x1,x2],[x1,y2]},{x3,y3}:] = { [[x1,x2],x3],[[x1,x2],y3],[[x1,y2],x3],[[x1,y2],y3]} by Th25 .= { [[x1,x2],x3],[[x1,y2],x3],[[x1,x2],y3],[[x1,y2],y3]} by ENUMSET1:104 .= { [x1,x2,x3],[[x1,y2],x3],[[x1,x2],y3],[[x1,y2],y3]} by Def3 .= { [x1,x2,x3],[x1,y2,x3],[[x1,x2],y3],[[x1,y2],y3]} by Def3 .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[[x1,y2],y3]} by Def3 .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]} by Def3; A2: [:{[y1,x2],[y1,y2]},{x3,y3}:] = { [[y1,x2],x3],[[y1,x2],y3],[[y1,y2],x3],[[y1,y2],y3]} by Th25 .= { [[y1,x2],x3],[[y1,y2],x3],[[y1,x2],y3],[[y1,y2],y3]} by ENUMSET1:104 .= { [y1,x2,x3],[[y1,y2],x3],[[y1,x2],y3],[[y1,y2],y3]} by Def3 .= { [y1,x2,x3],[y1,y2,x3],[[y1,x2],y3],[[y1,y2],y3]} by Def3 .= { [y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[[y1,y2],y3]} by Def3 .= { [y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3]} by Def3; thus [:{x1,y1},{x2,y2},{x3,y3}:] = [:[:{x1,y1},{x2,y2}:],{x3,y3}:] by ZFMISC_1:def 3 .= [:{[x1,x2],[x1,y2],[y1,x2],[y1,y2]},{x3,y3}:] by Th25 .= [:{[x1,x2],[x1,y2]} \/ {[y1,x2],[y1,y2]},{x3,y3}:] by ENUMSET1:45 .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]} \/ {[y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3] } by A1,A2,ZFMISC_1:120 .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3], [y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3] } by ENUMSET1:65; end; definition let X1,X2,X3; assume A1: X1<>{} & X2<>{} & X3<>{}; let x be Element of [:X1,X2,X3:]; func x`1 -> Element of X1 means :Def5: x = [x1,x2,x3] implies it = x1; existence proof consider xx1,xx2,xx3 such that A2: x = [xx1,xx2,xx3] by A1,Lm2; take xx1; thus thesis by A2,Th28; end; uniqueness proof consider xx1,xx2,xx3 such that A3: x = [xx1,xx2,xx3] by A1,Lm2; let y,z be Element of X1; assume x = [x1,x2,x3] implies y = x1; then A4: y = xx1 by A3; assume x = [x1,x2,x3] implies z = x1; hence thesis by A3,A4; end; func x`2 -> Element of X2 means :Def6: x = [x1,x2,x3] implies it = x2; existence proof consider xx1,xx2,xx3 such that A5: x = [xx1,xx2,xx3] by A1,Lm2; take xx2; thus thesis by A5,Th28; end; uniqueness proof consider xx1,xx2,xx3 such that A6: x = [xx1,xx2,xx3] by A1,Lm2; let y,z be Element of X2; assume x = [x1,x2,x3] implies y = x2; then A7: y = xx2 by A6; assume x = [x1,x2,x3] implies z = x2; hence thesis by A6,A7; end; func x`3 -> Element of X3 means :Def7: x = [x1,x2,x3] implies it = x3; existence proof consider xx1,xx2,xx3 such that A8: x = [xx1,xx2,xx3] by A1,Lm2; take xx3; thus thesis by A8,Th28; end; uniqueness proof consider xx1,xx2,xx3 such that A9: x = [xx1,xx2,xx3] by A1,Lm2; let y,z be Element of X3; assume x = [x1,x2,x3] implies y = x3; then A10: y = xx3 by A9; assume x = [x1,x2,x3] implies z = x3; hence thesis by A9,A10; end; end; theorem X1<>{} & X2<>{} & X3<>{} implies for x being Element of [:X1,X2,X3:] for x1,x2,x3 st x = [x1,x2,x3] holds x`1 = x1 & x`2 = x2 & x`3 = x3 by Def5,Def6,Def7; theorem Th48: X1<>{} & X2<>{} & X3<>{} implies for x being Element of [:X1,X2,X3:] holds x = [x`1,x`2,x`3] proof assume A1: X1<>{} & X2<>{} & X3<>{}; let x be Element of [:X1,X2,X3:]; consider xx1,xx2,xx3 such that A2: x = [xx1,xx2,xx3] by A1,Lm2; thus x = [x`1,xx2,xx3] by A1,A2,Def5 .= [x`1,x`2,xx3] by A1,A2,Def6 .= [x`1,x`2,x`3] by A1,A2,Def7; end; theorem Th49: X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] implies X = {} proof assume that A1: X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] and A2: X <> {}; [:X,Y,Z:]<>{} or [:Y,Z,X:]<>{} or [:Z,X,Y:]<>{} by A1,A2,XBOOLE_1:3; then A3: X<>{} & Y<>{} & Z<>{} by Th35; now per cases by A1; suppose A4: X c= [:X,Y,Z:]; consider v such that A5: v in X and A6: for x,y,z st x in X or y in X holds v <> [x,y,z] by A2,Th29; reconsider v as Element of [:X,Y,Z:] by A4,A5; v = [v`1,v`2,v`3] & v`1 in X by A3,Th48; hence contradiction by A6; suppose X c= [:Y,Z,X:]; then X c= [:[:Y,Z:],X:] by ZFMISC_1:def 3; hence thesis by A2,ZFMISC_1:135; suppose A7: X c= [:Z,X,Y:]; consider v such that A8: v in X and A9: for z,x,y st z in X or x in X holds v <> [z,x,y] by A2,Th29; reconsider v as Element of [:Z,X,Y:] by A7,A8; v = [v`1,v`2,v`3] & v`2 in X by A3,Th48; hence thesis by A9; end; hence contradiction; end; theorem Th50: X1<>{} & X2<>{} & X3<>{} implies for x being Element of [:X1,X2,X3:] holds x`1 = (x qua set)`1`1 & x`2 = (x qua set)`1`2 & x`3 = (x qua set)`2 proof assume A1: X1<>{} & X2<>{} & X3<>{}; let x be Element of [:X1,X2,X3:]; thus x`1 = [x`1,x`2]`1 by Def1 .= [[x`1,x`2],x`3]`1`1 by Def1 .= [x`1,x`2,x`3]`1`1 by Def3 .= (x qua set)`1`1 by A1,Th48; thus x`2 = [x`1,x`2]`2 by Def2 .= [[x`1,x`2],x`3]`1`2 by Def1 .= [x`1,x`2,x`3]`1`2 by Def3 .= (x qua set)`1`2 by A1,Th48; thus x`3 = [[x`1,x`2],x`3]`2 by Def2 .= [x`1,x`2,x`3]`2 by Def3 .= (x qua set)`2 by A1,Th48; end; theorem Th51: X1<>{} & X2<>{} & X3<>{} implies for x being Element of [:X1,X2,X3:] holds x <> x`1 & x <> x`2 & x <> x`3 proof assume A1: X1<>{} & X2<>{} & X3<>{}; let x be Element of [:X1,X2,X3:]; set Y' = { x`1,x`2 }, Y = { Y',{x`1}}, X' = { Y,x`3 }, X = { X',{Y} }; A2: x = [x`1,x`2,x`3] by A1,Th48 .= [[x`1,x`2],x`3] by Def3; then x = [ Y,x`3 ] by TARSKI:def 5 .= X by TARSKI:def 5; then x = x`1 or x = x`2 implies X in Y' & Y' in Y & Y in X' & X' in X by TARSKI:def 2; hence x <> x`1 & x <> x`2 by ORDINAL1:4; x`3 = (x qua set)`2 by A1,Th50; hence x <> x`3 by A2,Th20; end; theorem [:X1,X2,X3:] meets [:Y1,Y2,Y3:] implies X1 meets Y1 & X2 meets Y2 & X3 meets Y3 proof A1: [:[:X1,X2:],X3:] = [:X1,X2,X3:] & [:[:Y1,Y2:],Y3:] = [:Y1,Y2,Y3:] by ZFMISC_1:def 3; assume [:X1,X2,X3:] meets [:Y1,Y2,Y3:]; then [:X1,X2:] meets [:Y1,Y2:] & X3 meets Y3 by A1,ZFMISC_1:127; hence thesis by ZFMISC_1:127; end; :: :: Cartesian products of four sets :: theorem Th53: [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:] proof thus [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4 .= [:[:[:X1,X2:],X3:],X4:] by ZFMISC_1:def 3; end; theorem Th54: [:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:] proof thus [:[:X1,X2:],X3,X4:] = [:[:[:X1,X2:],X3:],X4:] by ZFMISC_1:def 3 .= [:X1,X2,X3,X4:] by Th53; end; theorem Th55: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} iff [:X1,X2,X3,X4:] <> {} proof A1: [:[:X1,X2,X3:],X4:] = [:X1,X2,X3,X4:] by ZFMISC_1:def 4; X1 <> {} & X2 <> {} & X3 <> {} iff [:X1,X2,X3:] <> {} by Th35; hence thesis by A1,ZFMISC_1:113; end; theorem Th56: X1<>{} & X2<>{} & X3<>{} & X4<>{} implies ( [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4) proof A1: [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4; assume A2: X1<>{} & X2<>{} & X3<>{}; then A3: [:X1,X2,X3:] <> {} by Th35; assume A4: X4<>{}; assume [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:]; then [:[:X1,X2,X3:],X4:] = [:[:Y1,Y2,Y3:],Y4:] by A1,ZFMISC_1:def 4; then [:X1,X2,X3:] = [:Y1,Y2,Y3:] & X4 = Y4 by A3,A4,ZFMISC_1:134; hence thesis by A2,Th36; end; theorem [:X1,X2,X3,X4:]<>{} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 proof assume [:X1,X2,X3,X4:]<>{}; then X1<>{} & X2<>{} & X3<>{} & X4<>{} by Th55; hence thesis by Th56; end; theorem [:X,X,X,X:] = [:Y,Y,Y,Y:] implies X = Y proof assume [:X,X,X,X:] = [:Y,Y,Y,Y:]; then X<>{} or Y<>{} implies thesis by Th56; hence X = Y; end; reserve xx4 for Element of X4; 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 Th35; 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,Def4; end; definition let X1,X2,X3,X4; assume A1: X1<>{} & X2<>{} & X3<>{} & X4 <> {}; let x be Element of [:X1,X2,X3,X4:]; func x`1 -> Element of X1 means :Def8: x = [x1,x2,x3,x4] implies it = x1; existence proof consider xx1,xx2,xx3,xx4 such that A2: x = [xx1,xx2,xx3,xx4] by A1,Lm3; take xx1; thus thesis by A2,Th33; end; uniqueness proof consider xx1,xx2,xx3,xx4 such that A3: x = [xx1,xx2,xx3,xx4] by A1,Lm3; let y,z be Element of X1; assume x = [x1,x2,x3,x4] implies y = x1; then A4: y = xx1 by A3; assume x = [x1,x2,x3,x4] implies z = x1; hence thesis by A3,A4; end; func x`2 -> Element of X2 means :Def9: x = [x1,x2,x3,x4] implies it = x2; existence proof consider xx1,xx2,xx3,xx4 such that A5: x = [xx1,xx2,xx3,xx4] by A1,Lm3; take xx2; thus thesis by A5,Th33; end; uniqueness proof consider xx1,xx2,xx3,xx4 such that A6: x = [xx1,xx2,xx3,xx4] by A1,Lm3; let y,z be Element of X2; assume x = [x1,x2,x3,x4] implies y = x2; then A7: y = xx2 by A6; assume x = [x1,x2,x3,x4] implies z = x2; hence thesis by A6,A7; end; func x`3 -> Element of X3 means :Def10: x = [x1,x2,x3,x4] implies it = x3; existence proof consider xx1,xx2,xx3,xx4 such that A8: x = [xx1,xx2,xx3,xx4] by A1,Lm3; take xx3; thus thesis by A8,Th33; end; uniqueness proof consider xx1,xx2,xx3,xx4 such that A9: x = [xx1,xx2,xx3,xx4] by A1,Lm3; let y,z be Element of X3; assume x = [x1,x2,x3,x4] implies y = x3; then A10: y = xx3 by A9; assume x = [x1,x2,x3,x4] implies z = x3; hence thesis by A9,A10; end; func x`4 -> Element of X4 means :Def11: x = [x1,x2,x3,x4] implies it = x4; existence proof consider xx1,xx2,xx3,xx4 such that A11: x = [xx1,xx2,xx3,xx4] by A1,Lm3; take xx4; thus thesis by A11,Th33; end; uniqueness proof consider xx1,xx2,xx3,xx4 such that A12: x = [xx1,xx2,xx3,xx4] by A1,Lm3; let y,z be Element of X4; assume x = [x1,x2,x3,x4] implies y = x4; then A13: y = xx4 by A12; assume x = [x1,x2,x3,x4] implies z = x4; hence thesis by A12,A13; end; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} implies for x being Element of [:X1,X2,X3,X4:] for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 by Def8,Def9,Def10,Def11; theorem Th60: X1<>{} & X2<>{} & X3<>{} & X4<>{} implies for x being Element of [:X1,X2,X3,X4:] holds x = [x`1,x`2,x`3,x`4] proof assume A1: X1<>{} & X2<>{} & X3<>{} & X4<>{}; let x be Element of [:X1,X2,X3,X4:]; consider xx1,xx2,xx3,xx4 such that A2: x = [xx1,xx2,xx3,xx4] by A1,Lm3; thus x = [x`1,xx2,xx3,xx4] by A1,A2,Def8 .= [x`1,x`2,xx3,xx4] by A1,A2,Def9 .= [x`1,x`2,x`3,xx4] by A1,A2,Def10 .= [x`1,x`2,x`3,x`4] by A1,A2,Def11; end; theorem Th61: X1<>{} & X2<>{} & X3<>{} & X4<>{} implies for x being Element of [:X1,X2,X3,X4:] holds x`1 = (x qua set)`1`1`1 & x`2 = (x qua set)`1`1`2 & x`3 = (x qua set)`1`2 & x`4 = (x qua set)`2 proof assume A1: X1<>{} & X2<>{} & X3<>{} & X4<>{}; let x be Element of [:X1,X2,X3,X4:]; thus x`1 = [x`1,x`2]`1 by Def1 .= [[x`1,x`2],x`3]`1`1 by Def1 .= [x`1,x`2,x`3]`1`1 by Def3 .= [[x`1,x`2,x`3],x`4]`1`1`1 by Def1 .= [x`1,x`2,x`3,x`4]`1`1`1 by Def4 .= (x qua set)`1`1`1 by A1,Th60; thus x`2 = [x`1,x`2]`2 by Def2 .= [[x`1,x`2],x`3]`1`2 by Def1 .= [x`1,x`2,x`3]`1`2 by Def3 .= [[x`1,x`2,x`3],x`4]`1`1`2 by Def1 .= [x`1,x`2,x`3,x`4]`1`1`2 by Def4 .= (x qua set)`1`1`2 by A1,Th60; thus x`3 = [[x`1,x`2],x`3]`2 by Def2 .= [x`1,x`2,x`3]`2 by Def3 .= [[x`1,x`2,x`3],x`4]`1`2 by Def1 .= [x`1,x`2,x`3,x`4]`1`2 by Def4 .= (x qua set)`1`2 by A1,Th60; thus x`4 = [[x`1,x`2,x`3],x`4]`2 by Def2 .= [x`1,x`2,x`3,x`4]`2 by Def4 .= (x qua set)`2 by A1,Th60; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} implies for x being Element of [:X1,X2,X3,X4:] holds x <> x`1 & x <> x`2 & x <> x`3 & x <> x`4 proof assume A1: X1<>{} & X2<>{} & X3<>{} & X4<>{}; then A2: [:X1,X2:] <> {} by ZFMISC_1:113; let x be Element of [:X1,X2,X3,X4:]; set Z' = { x`1,x`2 }, Z = { Z',{x`1}}, Y' = { Z,x`3 }, Y = { Y',{Z} }, X' = { Y,x`4 }, X = { X',{Y} }; x = [x`1,x`2,x`3,x`4] by A1,Th60 .= [[[x`1,x`2],x`3],x`4] by Th31 .= [ [Z,x`3],x`4 ] by TARSKI:def 5 .= [ Y,x`4 ] by TARSKI:def 5 .= X by TARSKI:def 5; then x = x`1 or x = x`2 implies X in Z' & Z' in Z & Z in Y' & Y' in Y & Y in X' & X' in X by TARSKI:def 2; hence x <> x`1 & x <> x`2 by ORDINAL1:6; reconsider x'=x as Element of [:[:X1,X2:],X3,X4:] by Th54; A3: x`3 = (x qua set)`1`2 by A1,Th61 .= x'`2 by A1,A2,Th50; x`4 = (x qua set)`2 by A1,Th61 .= x'`3 by A1,A2,Th50; hence thesis by A1,A2,A3,Th51; end; theorem X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2:] or X1 c= [:X4,X1,X2,X3:] implies X1 = {} proof assume that A1: X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2:] or X1 c= [:X4,X1,X2,X3:] and A2: X1 <> {}; [:X1,X2,X3,X4:]<>{} or [:X2,X3,X4,X1:]<>{} or [:X3,X4,X1,X2:]<>{} or [:X4,X1,X2,X3:]<>{} by A1,A2,XBOOLE_1:3; then A3: X1<>{} & X2<>{} & X3<>{} & X4<>{} by Th55; now per cases by A1; suppose A4: X1 c= [:X1,X2,X3,X4:]; consider v such that A5: v in X1 and A6: for x1,x2,x3,x4 st x1 in X1 or x2 in X1 holds v <> [x1,x2,x3,x4] by A2,Th34; reconsider v as Element of [:X1,X2,X3,X4:] by A4,A5; v = [v`1,v`2,v`3,v`4] & v`1 in X1 by A3,Th60; hence contradiction by A6; suppose X1 c= [:X2,X3,X4,X1:]; then X1 c= [:[:X2,X3:],X4,X1:] by Th54; hence thesis by A2,Th49; suppose X1 c= [:X3,X4,X1,X2:]; then X1 c= [:[:X3,X4:],X1,X2:] by Th54; hence thesis by A2,Th49; suppose A7: X1 c= [:X4,X1,X2,X3:]; consider v such that A8: v in X1 and A9: for x1,x2,x3,x4 st x1 in X1 or x2 in X1 holds v <> [x1,x2,x3,x4] by A2,Th34; reconsider v as Element of [:X4,X1,X2,X3:] by A7,A8; v = [v`1,v`2,v`3,v`4] & v`2 in X1 by A3,Th60; hence thesis by A9; end; hence contradiction; end; theorem [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:] implies X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 proof A1: [:[:[:X1,X2:],X3:],X4:] = [:X1,X2,X3,X4:] & [:[:[:Y1,Y2:],Y3:],Y4:] = [:Y1,Y2,Y3,Y4:] by Th53; assume [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:]; then [:[:X1,X2:],X3:] meets [:[:Y1,Y2:],Y3:] & X4 meets Y4 by A1,ZFMISC_1:127; then [:X1,X2:] meets [:Y1,Y2:] & X3 meets Y3 & X4 meets Y4 by ZFMISC_1:127; hence thesis by ZFMISC_1:127; end; theorem [:{x1},{x2},{x3},{x4}:] = { [x1,x2,x3,x4] } proof thus [:{x1},{x2},{x3},{x4}:] = [:[:{x1},{x2}:],{x3},{x4}:] by Th54 .= [:{[x1,x2]},{x3},{x4}:] by ZFMISC_1:35 .= {[[x1,x2],x3,x4]} by Th39 .= { [x1,x2,x3,x4] }by Th32; end; :: Ordered pairs theorem Th66: [:X,Y:] <> {} implies for x being Element of [:X,Y:] holds x <> x`1 & x <> x`2 proof assume [:X,Y:] <> {}; then X <> {} & Y <> {} by ZFMISC_1:113; hence thesis by Th26; end; theorem x in [:X,Y:] implies x <> x`1 & x <> x`2 by Th66; :: Triples reserve A1 for Subset of X1, A2 for Subset of X2, A3 for Subset of X3, A4 for Subset of X4; reserve x for Element of [:X1,X2,X3:]; theorem X1<>{} & X2<>{} & X3<>{} implies for x1,x2,x3 st x = [x1,x2,x3] holds x`1 = x1 & x`2 = x2 & x`3 = x3 by Def5, Def6,Def7; theorem X1<>{} & X2<>{} & X3<>{} & (for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y1 = xx1) implies y1 =x`1 proof assume that A1: X1<>{} & X2<>{} & X3<>{} and A2: for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y1 = xx1; x = [x`1,x`2,x`3] by A1,Th48; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & (for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y2 = xx2) implies y2 =x`2 proof assume that A1: X1<>{} & X2<>{} & X3<>{} and A2: for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y2 = xx2; x = [x`1,x`2,x`3] by A1,Th48; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & (for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y3 = xx3) implies y3 =x`3 proof assume that A1: X1<>{} & X2<>{} & X3<>{} and A2: for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y3 = xx3; x = [x`1,x`2,x`3] by A1,Th48; hence thesis by A2; end; theorem Th72: z in [: X1,X2,X3 :] implies ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] proof assume z in [: X1,X2,X3 :]; then z in [:[:X1,X2:],X3:] by ZFMISC_1:def 3; then consider x12, x3 being set such that A1: x12 in [:X1,X2:] and A2: x3 in X3 and A3: z = [x12,x3] by ZFMISC_1:def 2; consider x1,x2 being set such that A4: x1 in X1 and A5: x2 in X2 and A6: x12 = [x1,x2] by A1,ZFMISC_1:def 2; z = [x1,x2,x3] by A3,A6,Def3; hence thesis by A2,A4,A5; end; theorem Th73: [x1,x2,x3] in [: X1,X2,X3 :] iff x1 in X1 & x2 in X2 & x3 in X3 proof A1: [:X1,X2,X3:] = [:[:X1,X2:],X3:] by ZFMISC_1:def 3; A2: [x1,x2,x3] = [[x1,x2],x3] by Def3; [x1,x2] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:106; hence thesis by A1,A2,ZFMISC_1:106; end; theorem (for z holds z in Z iff ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3]) implies Z = [: X1,X2,X3 :] proof assume A1: for z holds z in Z iff ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3]; now let z; thus z in Z implies z in [:[:X1,X2:],X3:] proof assume z in Z; then consider x1,x2,x3 such that A2: x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] by A1; A3: z = [[x1,x2],x3] by A2,Def3; [x1,x2] in [:X1,X2:] & x3 in X3 by A2,ZFMISC_1:def 2; hence z in [:[:X1,X2:],X3:] by A3,ZFMISC_1:def 2; end; assume z in [:[:X1,X2:],X3:]; then consider x12,x3 being set such that A4: x12 in [:X1,X2:] and A5: x3 in X3 and A6: z = [x12,x3] by ZFMISC_1:def 2; consider x1,x2 being set such that A7: x1 in X1 and A8: x2 in X2 and A9: x12 = [x1,x2] by A4,ZFMISC_1:def 2; z = [x1,x2,x3] by A6,A9,Def3; hence z in Z by A1,A5,A7,A8; end; then Z = [:[:X1,X2:],X3:] by TARSKI:2; hence Z = [: X1,X2,X3 :] by ZFMISC_1:def 3; end; theorem Th75: X1 <> {} & X2 <> {} & X3 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} implies for x being (Element of [:X1,X2,X3:]), y being Element of [:Y1,Y2,Y3:] holds x = y implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3 proof assume that A1: X1 <> {} & X2 <> {} & X3 <> {} and A2: Y1 <> {} & Y2 <> {} & Y3 <> {}; let x be Element of [:X1,X2,X3:]; let y be Element of [:Y1,Y2,Y3:]; assume A3: x = y; thus x`1 = (x qua set)`1`1 by A1,Th50 .= y`1 by A2,A3,Th50; thus x`2 = (x qua set)`1`2 by A1,Th50 .= y`2 by A2,A3,Th50; thus x`3 = (x qua set)`2 by A1,Th50 .= y`3 by A2,A3,Th50; end; theorem for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:] holds x`1 in A1 & x`2 in A2 & x`3 in A3 proof let x be Element of [:X1,X2,X3:]; assume A1: x in [:A1,A2,A3:]; then A2: A1 <> {} & A2 <> {} & A3 <> {} by Th35; reconsider y = x as Element of [:A1,A2,A3:] by A1; y`1 in A1 & y`2 in A2 & y`3 in A3 by A2; hence x`1 in A1 & x`2 in A2 & x`3 in A3 by Th75; end; theorem Th77: X1 c= Y1 & X2 c= Y2 & X3 c= Y3 implies [:X1,X2,X3:] c= [:Y1,Y2,Y3:] proof assume X1 c= Y1 & X2 c= Y2; then A1: [:X1,X2:] c= [:Y1,Y2:] by ZFMISC_1:119; A2: [:X1,X2,X3:] = [:[:X1,X2:],X3:] & [:Y1,Y2,Y3:] = [:[:Y1,Y2:],Y3:] by ZFMISC_1:def 3; assume X3 c= Y3; hence thesis by A1,A2,ZFMISC_1:119; end; :: Quadruples reserve x for Element of [:X1,X2,X3,X4:]; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} implies for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 by Def8,Def9,Def10,Def11; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & (for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1) implies y1 =x`1 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} and A2: for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1; x = [x`1,x`2,x`3,x`4] by A1,Th60; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & (for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y2 = xx2) implies y2 =x`2 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} and A2: for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y2 = xx2; x = [x`1,x`2,x`3,x`4] by A1,Th60; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & (for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y3 = xx3) implies y3 =x`3 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} and A2: for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y3 = xx3; x = [x`1,x`2,x`3,x`4] by A1,Th60; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & (for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y4 = xx4) implies y4 =x`4 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} and A2: for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y4 = xx4; x = [x`1,x`2,x`3,x`4] by A1,Th60; hence thesis by A2; end; theorem z in [: X1,X2,X3,X4 :] implies ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] proof assume z in [: X1,X2,X3,X4 :]; then z in [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4; then consider x123, x4 being set such that A1: x123 in [:X1,X2,X3:] and A2: x4 in X4 and A3: z = [x123,x4] by ZFMISC_1:def 2; consider x1, x2, x3 such that A4: x1 in X1 & x2 in X2 & x3 in X3 & x123 = [x1,x2,x3] by A1,Th72; z = [x1,x2,x3,x4] by A3,A4,Def4; hence thesis by A2,A4; end; theorem [x1,x2,x3,x4] in [: X1,X2,X3,X4 :] iff x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 proof A1: [:X1,X2,X3,X4:] = [:[:X1,X2:],X3,X4:] by Th54; A2: [x1,x2,x3,x4] = [[x1,x2],x3,x4] by Th32; [x1,x2] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:106; hence thesis by A1,A2,Th73; end; theorem (for z holds z in Z iff ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4]) implies Z = [: X1,X2,X3,X4 :] proof assume A1: for z holds z in Z iff ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4]; now let z; thus z in Z implies z in [:[:X1,X2,X3:],X4:] proof assume z in Z; then consider x1,x2,x3,x4 such that A2: x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] by A1; A3: z = [[x1,x2,x3],x4] by A2,Def4; [x1,x2,x3] in [:X1,X2,X3:] & x4 in X4 by A2,Th73; hence z in [:[:X1,X2,X3:],X4:] by A3,ZFMISC_1:def 2; end; assume z in [:[:X1,X2,X3:],X4:]; then consider x123,x4 being set such that A4: x123 in [:X1,X2,X3:] and A5: x4 in X4 and A6: z = [x123,x4] by ZFMISC_1:def 2; consider x1,x2,x3 such that A7: x1 in X1 & x2 in X2 & x3 in X3 & x123 = [x1,x2,x3] by A4,Th72; z = [x1,x2,x3,x4] by A6,A7,Def4; hence z in Z by A1,A5,A7; end; then Z = [:[:X1,X2,X3:],X4:] by TARSKI:2; hence Z = [: X1,X2,X3,X4 :] by ZFMISC_1:def 4; end; theorem Th86: X1<>{} & X2<>{} & X3<>{} & X4<>{} & Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} implies for x being (Element of [:X1,X2,X3,X4:]), y being Element of [:Y1,Y2,Y3,Y4:] holds x = y implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3 & x`4 = y`4 proof assume that A1: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} and A2: Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {}; let x be Element of [:X1,X2,X3,X4:]; let y be Element of [:Y1,Y2,Y3,Y4:]; assume A3: x = y; thus x`1 = (x qua set)`1`1`1 by A1,Th61 .= y`1 by A2,A3,Th61; thus x`2 = (x qua set)`1`1`2 by A1,Th61 .= y`2 by A2,A3,Th61; thus x`3 = (x qua set)`1`2 by A1,Th61 .= y`3 by A2,A3,Th61; thus x`4 = (x qua set)`2 by A1,Th61 .= y`4 by A2,A3,Th61; end; theorem for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4 proof let x be Element of [:X1,X2,X3,X4:]; assume A1: x in [:A1,A2,A3,A4:]; then A2: A1 <> {} & A2 <> {} & A3 <> {} & A4 <> {} by Th55; reconsider y = x as Element of [:A1,A2,A3,A4:] by A1; y`1 in A1 & y`2 in A2 & y`3 in A3 & y`4 in A4 by A2; hence x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4 by Th86; end; theorem Th88: X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 implies [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:] proof assume X1 c= Y1 & X2 c= Y2 & X3 c= Y3; then A1: [:X1,X2,X3:] c= [:Y1,Y2,Y3:] by Th77; A2: [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] & [:Y1,Y2,Y3,Y4:] = [:[:Y1,Y2,Y3:],Y4:] by ZFMISC_1:def 4; assume X4 c= Y4; hence thesis by A1,A2,ZFMISC_1:119; end; definition let X1,X2,A1,A2; redefine func [:A1,A2:] -> Subset of [:X1,X2:]; coherence by ZFMISC_1:119; end; definition let X1,X2,X3,A1,A2,A3; redefine func [:A1,A2,A3:] -> Subset of [:X1,X2,X3:]; coherence by Th77; end; definition let X1,X2,X3,X4,A1,A2,A3,A4; redefine func [:A1,A2,A3,A4:] -> Subset of [:X1,X2,X3,X4:]; coherence by Th88; end;

Back to top