:: N-Tuples and Cartesian Products for n=5
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received October 13, 1990
:: Copyright (c) 1990 Association of Mizar Users

Lm1: for X1, X2 being set st X1 <> {} & X2 <> {} holds
for x being Element of [:X1,X2:] ex xx1 being Element of X1 ex xx2 being Element of X2 st x = [xx1,xx2]

proof end;

Lm2: for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds
for x being Element of [:X1,X2,X3:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3]

proof end;

Lm3: for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
for x being Element of [:X1,X2,X3,X4:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4]

proof end;

theorem :: MCART_2:1

for X being set st X <> {} holds
ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y holds
Y1 misses X ) )

proof end;

theorem Th2: :: MCART_2:2

for X being set st X <> {} holds
ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y holds
Y1 misses X ) )

proof end;

definition

let x1, x2, x3, x4, x5 be set ;
func [x1,x2,x3,x4,x5] -> set equals :: MCART_2:def 1
[[x1,x2,x3,x4],x5];
correctness
coherence
[[x1,x2,x3,x4],x5] is set ;
;

end;

:: deftheorem defines [ MCART_2:def 1 :

for x1, x2, x3, x4, x5 being set holds [x1,x2,x3,x4,x5] = [[x1,x2,x3,x4],x5];

theorem Th3: :: MCART_2:3

for x1, x2, x3, x4, x5 being set holds [x1,x2,x3,x4,x5] = [[[[x1,x2],x3],x4],x5]

proof end;

theorem :: MCART_2:4

canceled;

theorem :: MCART_2:5

for x1, x2, x3, x4, x5 being set holds [x1,x2,x3,x4,x5] = [[x1,x2,x3],x4,x5]

proof end;

theorem Th6: :: MCART_2:6

for x1, x2, x3, x4, x5 being set holds [x1,x2,x3,x4,x5] = [[x1,x2],x3,x4,x5]

proof end;

theorem Th7: :: MCART_2:7

for x1, x2, x3, x4, x5, y1, y2, y3, y4, y5 being set st [x1,x2,x3,x4,x5] = [y1,y2,y3,y4,y5] holds
( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 )

proof end;

theorem Th8: :: MCART_2:8

for X being set st X <> {} holds
ex x being set st
( x in X & ( for x1, x2, x3, x4, x5 being set holds
( ( not x1 in X & not x2 in X ) or not x = [x1,x2,x3,x4,x5] ) ) )

proof end;

definition

let X1, X2, X3, X4, X5 be set ;
func [:X1,X2,X3,X4,X5:] -> set equals :: MCART_2:def 2
[:[:X1,X2,X3,X4:],X5:];
correctness
coherence
[:[:X1,X2,X3,X4:],X5:] is set ;
;

end;

:: deftheorem defines [: MCART_2:def 2 :

for X1, X2, X3, X4, X5 being set holds [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3,X4:],X5:];

theorem Th9: :: MCART_2:9

for X1, X2, X3, X4, X5 being set holds [:X1,X2,X3,X4,X5:] = [:[:[:[:X1,X2:],X3:],X4:],X5:]

proof end;

theorem :: MCART_2:10

canceled;

theorem :: MCART_2:11

for X1, X2, X3, X4, X5 being set holds [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3:],X4,X5:]

proof end;

theorem Th12: :: MCART_2:12

for X1, X2, X3, X4, X5 being set holds [:X1,X2,X3,X4,X5:] = [:[:X1,X2:],X3,X4,X5:]

proof end;

theorem Th13: :: MCART_2:13

for X1, X2, X3, X4, X5 being set holds
( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} ) iff [:X1,X2,X3,X4,X5:] <> {} )

proof end;

theorem Th14: :: MCART_2:14

for X1, X2, X3, X4, X5, Y1, Y2, Y3, Y4, Y5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:] holds
( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 )

proof end;

theorem :: MCART_2:15

for X1, X2, X3, X4, X5, Y1, Y2, Y3, Y4, Y5 being set st [:X1,X2,X3,X4,X5:] <> {} & [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:] holds
( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 )

proof end;

theorem :: MCART_2:16

for X, Y being set st [:X,X,X,X,X:] = [:Y,Y,Y,Y,Y:] holds
X = Y

proof end;

theorem Th17: :: MCART_2:17

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5]

proof end;

definition

let X1, X2, X3, X4, X5 be set ;
assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} ) ;
let x be Element of [:X1,X2,X3,X4,X5:];
func x `1 -> Element of X1 means :Def3: :: MCART_2:def 3
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
it = x1;
existence
ex b₁ being Element of X1 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₁ = x1

proof end;

uniqueness
for b₁, b₂ being Element of X1 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₁ = x1 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₂ = x1 ) holds
b₁ = b₂

proof end;

func x `2 -> Element of X2 means :Def4: :: MCART_2:def 4
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
it = x2;
existence
ex b₁ being Element of X2 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₁ = x2

proof end;

uniqueness
for b₁, b₂ being Element of X2 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₁ = x2 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₂ = x2 ) holds
b₁ = b₂

proof end;

func x `3 -> Element of X3 means :Def5: :: MCART_2:def 5
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
it = x3;
existence
ex b₁ being Element of X3 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₁ = x3

proof end;

uniqueness
for b₁, b₂ being Element of X3 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₁ = x3 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₂ = x3 ) holds
b₁ = b₂

proof end;

func x `4 -> Element of X4 means :Def6: :: MCART_2:def 6
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
it = x4;
existence
ex b₁ being Element of X4 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₁ = x4

proof end;

uniqueness
for b₁, b₂ being Element of X4 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₁ = x4 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₂ = x4 ) holds
b₁ = b₂

proof end;

func x `5 -> Element of X5 means :Def7: :: MCART_2:def 7
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
it = x5;
existence
ex b₁ being Element of X5 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₁ = x5

proof end;

uniqueness
for b₁, b₂ being Element of X5 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₁ = x5 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₂ = x5 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines `1 MCART_2:def 3 :

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5:]
for b₇ being Element of X1 holds
( b₇ = x `1 iff for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₇ = x1 );

:: deftheorem Def4 defines `2 MCART_2:def 4 :

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5:]
for b₇ being Element of X2 holds
( b₇ = x `2 iff for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₇ = x2 );

:: deftheorem Def5 defines `3 MCART_2:def 5 :

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5:]
for b₇ being Element of X3 holds
( b₇ = x `3 iff for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₇ = x3 );

:: deftheorem Def6 defines `4 MCART_2:def 6 :

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5:]
for b₇ being Element of X4 holds
( b₇ = x `4 iff for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₇ = x4 );

:: deftheorem Def7 defines `5 MCART_2:def 7 :

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5:]
for b₇ being Element of X5 holds
( b₇ = x `5 iff for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b₇ = x5 );

theorem :: MCART_2:18

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5:]
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 ) by Def3, Def4, Def5, Def6, Def7;

theorem Th19: :: MCART_2:19

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5:] holds x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 )]

proof end;

theorem Th20: :: MCART_2:20

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5:] holds
( x `1 = (((x `1 ) `1 ) `1 ) `1 & x `2 = (((x `1 ) `1 ) `1 ) `2 & x `3 = ((x `1 ) `1 ) `2 & x `4 = (x `1 ) `2 & x `5 = x `2 )

proof end;

theorem :: MCART_2:21

for X1, X2, X3, X4, X5 being set st ( X1 c= [:X1,X2,X3,X4,X5:] or X1 c= [:X2,X3,X4,X5,X1:] or X1 c= [:X3,X4,X5,X1,X2:] or X1 c= [:X4,X5,X1,X2,X3:] or X1 c= [:X5,X1,X2,X3,X4:] ) holds
X1 = {}

proof end;

theorem :: MCART_2:22

for X1, X2, X3, X4, X5, Y1, Y2, Y3, Y4, Y5 being set st [:X1,X2,X3,X4,X5:] meets [:Y1,Y2,Y3,Y4,Y5:] holds
( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 )

proof end;

theorem :: MCART_2:23

for x1, x2, x3, x4, x5 being set holds [:{x1},{x2},{x3},{x4},{x5}:] = {[x1,x2,x3,x4,x5]}

proof end;

theorem :: MCART_2:24

for X1, X2, X3, X4, X5 being set
for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 ) by Def3, Def4, Def5, Def6, Def7;

theorem :: MCART_2:25

for X1, X2, X3, X4, X5, y1 being set
for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds
y1 = xx1 ) holds
y1 = x `1

proof end;

theorem :: MCART_2:26

for X1, X2, X3, X4, X5, y2 being set
for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds
y2 = xx2 ) holds
y2 = x `2

proof end;

theorem :: MCART_2:27

for X1, X2, X3, X4, X5, y3 being set
for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds
y3 = xx3 ) holds
y3 = x `3

proof end;

theorem :: MCART_2:28

for X1, X2, X3, X4, X5, y4 being set
for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds
y4 = xx4 ) holds
y4 = x `4

proof end;

theorem :: MCART_2:29

for X1, X2, X3, X4, X5, y5 being set
for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds
y5 = xx5 ) holds
y5 = x `5

proof end;

theorem :: MCART_2:30

for y, X1, X2, X3, X4, X5 being set st y in [:X1,X2,X3,X4,X5:] holds
ex x1, x2, x3, x4, x5 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & y = [x1,x2,x3,x4,x5] )

proof end;

theorem :: MCART_2:31

for x1, x2, x3, x4, x5, X1, X2, X3, X4, X5 being set holds
( [x1,x2,x3,x4,x5] in [:X1,X2,X3,X4,X5:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 ) )

proof end;

theorem :: MCART_2:32

for Z, X1, X2, X3, X4, X5 being set st ( for y being set holds
( y in Z iff ex x1, x2, x3, x4, x5 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & y = [x1,x2,x3,x4,x5] ) ) ) holds
Z = [:X1,X2,X3,X4,X5:]

proof end;

theorem Th33: :: MCART_2:33

for X1, X2, X3, X4, X5, Y1, Y2, Y3, Y4, Y5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {} & Y5 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5:]
for y being Element of [:Y1,Y2,Y3,Y4,Y5:] st x = y holds
( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 )

proof end;

theorem :: MCART_2:34

for X1, X2, X3, X4, X5 being set
for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4
for A5 being Subset of X5
for x being Element of [:X1,X2,X3,X4,X5:] st x in [:A1,A2,A3,A4,A5:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 )

proof end;

theorem Th35: :: MCART_2:35

for X1, Y1, X2, Y2, X3, Y3, X4, Y4, X5, Y5 being set st X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 holds
[:X1,X2,X3,X4,X5:] c= [:Y1,Y2,Y3,Y4,Y5:]

proof end;

definition

let X1, X2, X3, X4, X5 be set ;
let A1 be Subset of X1;
let A2 be Subset of X2;
let A3 be Subset of X3;
let A4 be Subset of X4;
let A5 be Subset of X5;
:: original: [:
redefine func [:A1,A2,A3,A4,A5:] -> Subset of [:X1,X2,X3,X4,X5:];
coherence
[:A1,A2,A3,A4,A5:] is Subset of [:X1,X2,X3,X4,X5:] by Th35;

end;

theorem :: MCART_2:36

for X1, X2 being set st X1 <> {} & X2 <> {} holds
for xx being Element of [:X1,X2:] ex xx1 being Element of X1 ex xx2 being Element of X2 st xx = [xx1,xx2] by Lm1;

theorem :: MCART_2:37

for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds
for xx being Element of [:X1,X2,X3:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st xx = [xx1,xx2,xx3] by Lm2;

theorem :: MCART_2:38

for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
for xx being Element of [:X1,X2,X3,X4:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 st xx = [xx1,xx2,xx3,xx4] by Lm3;