:: by Andrzej Trybulec

::

:: Received March 30, 1989

:: Copyright (c) 1990-2021 Association of Mizar Users

theorem :: MCART_1:9

for X being set st X <> {} holds

ex v being object st

( v in X & ( for x, y being object holds

( ( not x in X & not y in X ) or not v = [x,y] ) ) )

ex v being object st

( v in X & ( for x, y being object holds

( ( not x in X & not y in X ) or not v = [x,y] ) ) )

proof end;

:: Now we prove theorems describing relationships between projections

:: of ordered pairs and Cartesian products of two sets.

:: of ordered pairs and Cartesian products of two sets.

::$CT

theorem :: MCART_1:15

for x1, x2, z being object

for Y being set st z in [:{x1,x2},Y:] holds

( ( z `1 = x1 or z `1 = x2 ) & z `2 in Y )

for Y being set st z in [:{x1,x2},Y:] holds

( ( z `1 = x1 or z `1 = x2 ) & z `2 in Y )

proof end;

theorem :: MCART_1:16

for y1, y2, z being object

for X being set st z in [:X,{y1,y2}:] holds

( z `1 in X & ( z `2 = y1 or z `2 = y2 ) )

for X being set st z in [:X,{y1,y2}:] holds

( z `1 in X & ( z `2 = y1 or z `2 = y2 ) )

proof end;

theorem :: MCART_1:17

for x1, x2, y, z being object st z in [:{x1,x2},{y}:] holds

( ( z `1 = x1 or z `1 = x2 ) & z `2 = y )

( ( z `1 = x1 or z `1 = x2 ) & z `2 = y )

proof end;

theorem :: MCART_1:18

for x, y1, y2, z being object st z in [:{x},{y1,y2}:] holds

( z `1 = x & ( z `2 = y1 or z `2 = y2 ) )

( z `1 = x & ( z `2 = y1 or z `2 = y2 ) )

proof end;

theorem :: MCART_1:19

for x1, x2, y1, y2, z being object st z in [:{x1,x2},{y1,y2}:] holds

( ( z `1 = x1 or z `1 = x2 ) & ( z `2 = y1 or z `2 = y2 ) )

( ( z `1 = x1 or z `1 = x2 ) & ( z `2 = y1 or z `2 = y2 ) )

proof end;

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;

registration

let X1, X2 be non empty set ;

coherence

for b_{1} being Element of [:X1,X2:] holds b_{1} is pair

end;
coherence

for b

proof end;

theorem :: MCART_1:22

theorem Th18: :: MCART_1:24

for X, Y being set st X <> {} & Y <> {} holds

for x being Element of [:X,Y:] holds

( x <> x `1 & x <> x `2 )

for x being Element of [:X,Y:] holds

( x <> x `1 & x <> x `2 )

proof end;

::

:: Triples

::

::$CT

:: Triples

::

::$CT

theorem Th19: :: MCART_1:26

for X being set st X <> {} holds

ex v being object st

( v in X & ( for x, y, z being object holds

( ( not x in X & not y in X ) or not v = [x,y,z] ) ) )

ex v being object st

( v in X & ( for x, y, z being object holds

( ( not x in X & not y in X ) or not v = [x,y,z] ) ) )

proof end;

::

:: Quadruples

::

::$CT 3

:: Quadruples

::

::$CT 3

theorem Th20: :: MCART_1:30

for X being set st X <> {} holds

ex v being object st

( v in X & ( for x1, x2, x3, x4 being object holds

( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] ) ) )

ex v being object st

( v in X & ( for x1, x2, x3, x4 being object holds

( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] ) ) )

proof end;

::

:: Cartesian products of three sets

::

:: Cartesian products of three sets

::

theorem Th22: :: MCART_1:32

for X1, X2, X3, Y1, Y2, Y3 being set st X1 <> {} & X2 <> {} & X3 <> {} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 )

proof end;

theorem :: MCART_1:33

for X1, X2, X3, Y1, Y2, Y3 being set st [:X1,X2,X3:] <> {} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 )

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;

theorem :: MCART_1:39

for x1, x2, x3, y1, y2 being object holds [:{x1,y1},{x2,y2},{x3}:] = {[x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3]}

proof end;

theorem :: MCART_1:40

for x1, x2, x3, y1, y3 being object holds [:{x1,y1},{x2},{x3,y3}:] = {[x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3]}

proof end;

theorem :: MCART_1:41

for x1, x2, x3, y2, y3 being object holds [:{x1},{x2,y2},{x3,y3}:] = {[x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]}

proof end;

theorem :: MCART_1:42

for x1, x2, x3, y1, y2, y3 being object holds [:{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 end;

registration

let X1, X2, X3 be non empty set ;

coherence

for b_{1} being Element of [:X1,X2,X3:] holds b_{1} is triple

end;
coherence

for b

proof end;

definition

let X1, X2, X3 be non empty set ;

let x be Element of [:X1,X2,X3:];

x `1_3 is Element of X1

for b_{1} being Element of X1 holds

( b_{1} = x `1_3 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds

b_{1} = x1 )

x `2_3 is Element of X2

for b_{1} being Element of X2 holds

( b_{1} = x `2_3 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds

b_{1} = x2 )

x `2 is Element of X3

for b_{1} being Element of X3 holds

( b_{1} = x `2 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds

b_{1} = x3 )

end;
let x be Element of [:X1,X2,X3:];

:: original: `1_3

redefine func x `1_3 -> Element of X1 means :: MCART_1:def 5

for x1, x2, x3 being object st x = [x1,x2,x3] holds

it = x1;

coherence redefine func x `1_3 -> Element of X1 means :: MCART_1:def 5

for x1, x2, x3 being object st x = [x1,x2,x3] holds

it = x1;

x `1_3 is Element of X1

proof end;

compatibility for b

( b

b

proof end;

:: original: `2_3

redefine func x `2_3 -> Element of X2 means :: MCART_1:def 6

for x1, x2, x3 being object st x = [x1,x2,x3] holds

it = x2;

coherence redefine func x `2_3 -> Element of X2 means :: MCART_1:def 6

for x1, x2, x3 being object st x = [x1,x2,x3] holds

it = x2;

x `2_3 is Element of X2

proof end;

compatibility for b

( b

b

proof end;

:: original: `2

redefine func x `3_3 -> Element of X3 means :: MCART_1:def 7

for x1, x2, x3 being object st x = [x1,x2,x3] holds

it = x3;

coherence redefine func x `3_3 -> Element of X3 means :: MCART_1:def 7

for x1, x2, x3 being object st x = [x1,x2,x3] holds

it = x3;

x `2 is Element of X3

proof end;

compatibility for b

( b

b

proof end;

:: deftheorem defines `1_3 MCART_1:def 5 :

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:]

for b_{5} being Element of X1 holds

( b_{5} = x `1_3 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds

b_{5} = x1 );

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:]

for b

( b

b

:: deftheorem defines `2_3 MCART_1:def 6 :

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:]

for b_{5} being Element of X2 holds

( b_{5} = x `2_3 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds

b_{5} = x2 );

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:]

for b

( b

b

:: deftheorem defines `3_3 MCART_1:def 7 :

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:]

for b_{5} being Element of X3 holds

( b_{5} = x `3_3 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds

b_{5} = x3 );

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:]

for b

( b

b

::$CT 2

::$CT

theorem Th35: :: MCART_1:47

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] holds

( x <> x `1_3 & x <> x `2_3 & x <> x `3_3 )

for x being Element of [:X1,X2,X3:] holds

( x <> x `1_3 & x <> x `2_3 & x <> x `3_3 )

proof end;

theorem :: MCART_1:48

for X1, X2, X3, Y1, Y2, Y3 being set st [:X1,X2,X3:] meets [:Y1,Y2,Y3:] holds

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 )

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 )

proof end;

::

:: Cartesian products of four sets

::

:: Cartesian products of four sets

::

theorem Th39: :: MCART_1:51

for X1, X2, X3, X4 being set holds

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} )

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} )

proof end;

theorem Th40: :: MCART_1:52

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

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 )

proof end;

theorem :: MCART_1:53

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

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 )

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;

registration

let X1, X2, X3, X4 be non empty set ;

coherence

for b_{1} being Element of [:X1,X2,X3,X4:] holds b_{1} is quadruple

end;
coherence

for b

proof end;

definition

let X1, X2, X3, X4 be non empty set ;

let x be Element of [:X1,X2,X3,X4:];

x `1_4 is Element of X1

for b_{1} being Element of X1 holds

( b_{1} = x `1_4 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

b_{1} = x1 )

x `2_4 is Element of X2

for b_{1} being Element of X2 holds

( b_{1} = x `2_4 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

b_{1} = x2 )

x `2_3 is Element of X3

for b_{1} being Element of X3 holds

( b_{1} = x `2_3 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

b_{1} = x3 )

x `2 is Element of X4

for b_{1} being Element of X4 holds

( b_{1} = x `2 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

b_{1} = x4 )

end;
let x be Element of [:X1,X2,X3,X4:];

:: original: `1_4

redefine func x `1_4 -> Element of X1 means :: MCART_1:def 8

for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

it = x1;

coherence redefine func x `1_4 -> Element of X1 means :: MCART_1:def 8

for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

it = x1;

x `1_4 is Element of X1

proof end;

compatibility for b

( b

b

proof end;

:: original: `2_4

redefine func x `2_4 -> Element of X2 means :: MCART_1:def 9

for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

it = x2;

coherence redefine func x `2_4 -> Element of X2 means :: MCART_1:def 9

for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

it = x2;

x `2_4 is Element of X2

proof end;

compatibility for b

( b

b

proof end;

:: original: `2_3

redefine func x `3_4 -> Element of X3 means :: MCART_1:def 10

for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

it = x3;

coherence redefine func x `3_4 -> Element of X3 means :: MCART_1:def 10

for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

it = x3;

x `2_3 is Element of X3

proof end;

compatibility for b

( b

b

proof end;

:: original: `2

redefine func x `4_4 -> Element of X4 means :: MCART_1:def 11

for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

it = x4;

coherence redefine func x `4_4 -> Element of X4 means :: MCART_1:def 11

for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

it = x4;

x `2 is Element of X4

proof end;

compatibility for b

( b

b

proof end;

:: deftheorem defines `1_4 MCART_1:def 8 :

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:]

for b_{6} being Element of X1 holds

( b_{6} = x `1_4 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

b_{6} = x1 );

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:]

for b

( b

b

:: deftheorem defines `2_4 MCART_1:def 9 :

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:]

for b_{6} being Element of X2 holds

( b_{6} = x `2_4 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

b_{6} = x2 );

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:]

for b

( b

b

:: deftheorem defines `3_4 MCART_1:def 10 :

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:]

for b_{6} being Element of X3 holds

( b_{6} = x `3_4 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

b_{6} = x3 );

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:]

for b

( b

b

:: deftheorem defines `4_4 MCART_1:def 11 :

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:]

for b_{6} being Element of X4 holds

( b_{6} = x `4_4 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds

b_{6} = x4 );

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:]

for b

( b

b

::$CT 3

theorem :: MCART_1:58

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] holds

( x <> x `1_4 & x <> x `2_4 & x <> x `3_4 & x <> x `4_4 )

for x being Element of [:X1,X2,X3,X4:] holds

( x <> x `1_4 & x <> x `2_4 & x <> x `3_4 & x <> x `4_4 )

proof end;

theorem :: MCART_1:59

for X1, X2, X3, X4 being set st ( 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:] ) holds

X1 = {}

X1 = {}

proof end;

theorem :: MCART_1:60

for X1, X2, X3, X4, Y1, Y2, Y3, Y4 being set st [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:] holds

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 )

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 )

proof end;

:: Ordered pairs

theorem Th48: :: MCART_1:62

for X, Y being set st [:X,Y:] <> {} holds

for x being Element of [:X,Y:] holds

( x <> x `1 & x <> x `2 )

for x being Element of [:X,Y:] holds

( x <> x `1 & x <> x `2 )

proof end;

theorem :: MCART_1:63

theorem :: MCART_1:64

theorem :: MCART_1:65

for y1 being object

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds

y1 = xx1 ) holds

y1 = x `1_3

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds

y1 = xx1 ) holds

y1 = x `1_3

proof end;

theorem :: MCART_1:66

for y2 being object

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds

y2 = xx2 ) holds

y2 = x `2_3

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds

y2 = xx2 ) holds

y2 = x `2_3

proof end;

theorem :: MCART_1:67

for y3 being object

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds

y3 = xx3 ) holds

y3 = x `3_3

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds

y3 = xx3 ) holds

y3 = x `3_3

proof end;

theorem Th54: :: MCART_1:68

for z being object

for X1, X2, X3 being set st z in [:X1,X2,X3:] holds

ex x1, x2, x3 being object st

( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] )

for X1, X2, X3 being set st z in [:X1,X2,X3:] holds

ex x1, x2, x3 being object st

( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] )

proof end;

theorem Th55: :: MCART_1:69

for x1, x2, x3 being object

for X1, X2, X3 being set holds

( [x1,x2,x3] in [:X1,X2,X3:] iff ( x1 in X1 & x2 in X2 & x3 in X3 ) )

for X1, X2, X3 being set holds

( [x1,x2,x3] in [:X1,X2,X3:] iff ( x1 in X1 & x2 in X2 & x3 in X3 ) )

proof end;

theorem :: MCART_1:70

for X1, X2, X3, Z being set st ( for z being object holds

( z in Z iff ex x1, x2, x3 being object st

( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] ) ) ) holds

Z = [:X1,X2,X3:]

( z in Z iff ex x1, x2, x3 being object st

( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] ) ) ) holds

Z = [:X1,X2,X3:]

proof end;

::$CT

theorem :: MCART_1:72

for X1, X2, X3 being non empty set

for A1 being non empty Subset of X1

for A2 being non empty Subset of X2

for A3 being non empty Subset of X3

for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:] holds

( x `1_3 in A1 & x `2_3 in A2 & x `3_3 in A3 )

for A1 being non empty Subset of X1

for A2 being non empty Subset of X2

for A3 being non empty Subset of X3

for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:] holds

( x `1_3 in A1 & x `2_3 in A2 & x `3_3 in A3 )

proof end;

theorem Th58: :: MCART_1:73

for X1, X2, X3, Y1, Y2, Y3 being set st X1 c= Y1 & X2 c= Y2 & X3 c= Y3 holds

[:X1,X2,X3:] c= [:Y1,Y2,Y3:]

[:X1,X2,X3:] c= [:Y1,Y2,Y3:]

proof end;

theorem :: MCART_1:74

theorem :: MCART_1:75

for y1 being object

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds

y1 = xx1 ) holds

y1 = x `1_4

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds

y1 = xx1 ) holds

y1 = x `1_4

proof end;

theorem :: MCART_1:76

for y2 being object

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds

y2 = xx2 ) holds

y2 = x `2_4

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds

y2 = xx2 ) holds

y2 = x `2_4

proof end;

theorem :: MCART_1:77

for y3 being object

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds

y3 = xx3 ) holds

y3 = x `3_4

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds

y3 = xx3 ) holds

y3 = x `3_4

proof end;

theorem :: MCART_1:78

for y4 being object

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds

y4 = xx4 ) holds

y4 = x `4_4

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds

y4 = xx4 ) holds

y4 = x `4_4

proof end;

theorem :: MCART_1:79

for z being object

for X1, X2, X3, X4 being set st z in [:X1,X2,X3,X4:] holds

ex x1, x2, x3, x4 being object st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] )

for X1, X2, X3, X4 being set st z in [:X1,X2,X3,X4:] holds

ex x1, x2, x3, x4 being object st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] )

proof end;

theorem :: MCART_1:80

for x1, x2, x3, x4 being object

for X1, X2, X3, X4 being set holds

( [x1,x2,x3,x4] in [:X1,X2,X3,X4:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 ) )

for X1, X2, X3, X4 being set holds

( [x1,x2,x3,x4] in [:X1,X2,X3,X4:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 ) )

proof end;

theorem :: MCART_1:81

for X1, X2, X3, X4, Z being set st ( for z being object holds

( z in Z iff ex x1, x2, x3, x4 being object st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] ) ) ) holds

Z = [:X1,X2,X3,X4:]

( z in Z iff ex x1, x2, x3, x4 being object st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] ) ) ) holds

Z = [:X1,X2,X3,X4:]

proof end;

::$CT

theorem :: MCART_1:83

for X1, X2, X3, X4 being non empty set

for A1 being non empty Subset of X1

for A2 being non empty Subset of X2

for A3 being non empty Subset of X3

for A4 being non empty Subset of X4

for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds

( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 )

for A1 being non empty Subset of X1

for A2 being non empty Subset of X2

for A3 being non empty Subset of X3

for A4 being non empty Subset of X4

for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds

( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 )

proof end;

theorem Th68: :: MCART_1:84

for X1, X2, X3, X4, Y1, Y2, Y3, Y4 being set st X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 holds

[:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:]

[:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:]

proof end;

definition

let X1, X2 be set ;

let A1 be Subset of X1;

let A2 be Subset of X2;

:: original: [:

redefine func [:A1,A2:] -> Subset of [:X1,X2:];

coherence

[:A1,A2:] is Subset of [:X1,X2:] by ZFMISC_1:96;

end;
let A1 be Subset of X1;

let A2 be Subset of X2;

:: original: [:

redefine func [:A1,A2:] -> Subset of [:X1,X2:];

coherence

[:A1,A2:] is Subset of [:X1,X2:] by ZFMISC_1:96;

definition

let X1, X2, X3 be set ;

let A1 be Subset of X1;

let A2 be Subset of X2;

let A3 be Subset of X3;

:: original: [:

redefine func [:A1,A2,A3:] -> Subset of [:X1,X2,X3:];

coherence

[:A1,A2,A3:] is Subset of [:X1,X2,X3:] by Th58;

end;
let A1 be Subset of X1;

let A2 be Subset of X2;

let A3 be Subset of X3;

:: original: [:

redefine func [:A1,A2,A3:] -> Subset of [:X1,X2,X3:];

coherence

[:A1,A2,A3:] is Subset of [:X1,X2,X3:] by Th58;

definition

let X1, X2, X3, X4 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;

:: original: [:

redefine func [:A1,A2,A3,A4:] -> Subset of [:X1,X2,X3,X4:];

coherence

[:A1,A2,A3,A4:] is Subset of [:X1,X2,X3,X4:] by Th68;

end;
let A1 be Subset of X1;

let A2 be Subset of X2;

let A3 be Subset of X3;

let A4 be Subset of X4;

:: original: [:

redefine func [:A1,A2,A3,A4:] -> Subset of [:X1,X2,X3,X4:];

coherence

[:A1,A2,A3,A4:] is Subset of [:X1,X2,X3,X4:] by Th68;

:: from DTCONSTR

definition

let f be Function;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = (f . x) `1 ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = (f . x) `1 ) & dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = (f . x) `1 ) holds

b_{1} = b_{2}

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = (f . x) `2 ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = (f . x) `2 ) & dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = (f . x) `2 ) holds

b_{1} = b_{2}

end;
func pr1 f -> Function means :: MCART_1:def 12

( dom it = dom f & ( for x being object st x in dom f holds

it . x = (f . x) `1 ) );

existence ( dom it = dom f & ( for x being object st x in dom f holds

it . x = (f . x) `1 ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func pr2 f -> Function means :: MCART_1:def 13

( dom it = dom f & ( for x being object st x in dom f holds

it . x = (f . x) `2 ) );

existence ( dom it = dom f & ( for x being object st x in dom f holds

it . x = (f . x) `2 ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines pr1 MCART_1:def 12 :

for f, b_{2} being Function holds

( b_{2} = pr1 f iff ( dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = (f . x) `1 ) ) );

for f, b

( b

b

:: deftheorem defines pr2 MCART_1:def 13 :

for f, b_{2} being Function holds

( b_{2} = pr2 f iff ( dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = (f . x) `2 ) ) );

for f, b

( b

b

definition

let x be object ;

coherence

(x `1) `1 is set by TARSKI:1;

coherence

(x `1) `2 is set by TARSKI:1;

coherence

(x `2) `1 is set by TARSKI:1;

coherence

(x `2) `2 is set by TARSKI:1;

end;
coherence

(x `1) `1 is set by TARSKI:1;

coherence

(x `1) `2 is set by TARSKI:1;

coherence

(x `2) `1 is set by TARSKI:1;

coherence

(x `2) `2 is set by TARSKI:1;

theorem :: MCART_1:85

:: missing, 2007.04.13, A.T.

:: 2009.08.29, A.T.

theorem Th71: :: MCART_1:87

for R being non empty Relation

for x being object holds Im (R,x) = { (I `2) where I is Element of R : I `1 = x }

for x being object holds Im (R,x) = { (I `2) where I is Element of R : I `1 = x }

proof end;

theorem Th73: :: MCART_1:89

for y being object

for R being Relation

for x being object st x in R & y in R & x `1 = y `1 & x `2 = y `2 holds

x = y

for R being Relation

for x being object st x in R & y in R & x `1 = y `1 & x `2 = y `2 holds

x = y

proof end;

theorem :: MCART_1:90

:: 2010.05.120, A.T.

scheme :: MCART_1:sch 1

BiFuncEx{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , P_{1}[ object , object , object ] } :

BiFuncEx{ F

ex f, g being Function st

( dom f = F_{1}() & dom g = F_{1}() & ( for x being object st x in F_{1}() holds

P_{1}[x,f . x,g . x] ) )

provided( dom f = F

P

A1:
for x being object st x in F_{1}() holds

ex y, z being object st

( y in F_{2}() & z in F_{3}() & P_{1}[x,y,z] )

ex y, z being object st

( y in F

proof end;

theorem :: MCART_1:93

for x1, x2, x3, x4, y1, y2, y3, y4 being object st [[x1,x2],[x3,x4]] = [[y1,y2],[y3,y4]] holds

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )

proof 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.

::$CT 8