Copyright (c) 1989 Association of Mizar Users
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;