Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Tuples, Projections and Cartesian Products

**by****Andrzej Trybulec**- Received March 30, 1989
- MML identifier: MCART_1

- [ Mizar article, 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; 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 :: MCART_1:1 X <> {} implies ex Y st Y in X & Y misses X; theorem :: MCART_1:2 X <> {} implies ex Y st Y in X & for Y1 st Y1 in Y holds Y1 misses X; theorem :: MCART_1:3 X <> {} implies ex Y st Y in X & for Y1,Y2 st Y1 in Y2 & Y2 in Y holds Y1 misses X; theorem :: MCART_1:4 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; theorem :: MCART_1:5 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; theorem :: MCART_1:6 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; :: :: 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 x = [x1,x2]; func x`1 means :: MCART_1:def 1 x = [y1,y2] implies it = y1; func x`2 means :: MCART_1:def 2 x = [y1,y2] implies it = y2; end; theorem :: MCART_1:7 [x,y]`1=x & [x,y]`2=y; theorem :: MCART_1:8 (ex x,y st z=[x,y]) implies [z`1,z`2] =z; theorem :: MCART_1:9 X <> {} implies ex v st v in X & not ex x,y st (x in X or y in X) & v = [x,y]; :: Now we prove theorems describing relationships between projections :: of ordered pairs and Cartesian products of two sets. theorem :: MCART_1:10 z in [:X,Y:] implies z`1 in X & z`2 in Y; theorem :: MCART_1:11 (ex x,y st z=[x,y]) & z`1 in X & z`2 in Y implies z in [:X,Y:]; theorem :: MCART_1:12 z in [:{x},Y:] implies z`1=x & z`2 in Y; theorem :: MCART_1:13 z in [:X,{y}:] implies z`1 in X & z`2 = y; theorem :: MCART_1:14 z in [:{x},{y}:] implies z`1 = x & z`2 = y; theorem :: MCART_1:15 z in [:{x1,x2},Y:] implies (z`1=x1 or z`1=x2) & z`2 in Y; theorem :: MCART_1:16 z in [:X,{y1,y2}:] implies z`1 in X & (z`2 = y1 or z`2 = y2); theorem :: MCART_1:17 z in [:{x1,x2},{y}:] implies (z`1=x1 or z`1=x2) & z`2 = y; theorem :: MCART_1:18 z in [:{x},{y1,y2}:] implies z`1 = x & (z`2 = y1 or z`2 = y2); theorem :: MCART_1:19 z in [:{x1,x2},{y1,y2}:] implies (z`1 = x1 or z`1 = x2) & (z`2 = y1 or z`2 = y2); theorem :: MCART_1:20 (ex y,z st x = [y,z]) implies x <> x`1 & x <> x`2; :: 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 :: MCART_1:23 x in [:X,Y:] implies x = [x`1,x`2]; theorem :: MCART_1:24 X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x = [x`1,x`2]; theorem :: MCART_1:25 [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}; theorem :: MCART_1:26 X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x <> x`1 & x <> x`2; :: :: Triples :: definition let x1,x2,x3; func [x1,x2,x3] equals :: MCART_1:def 3 [[x1,x2],x3]; end; canceled; theorem :: MCART_1:28 [x1,x2,x3] = [y1,y2,y3] implies x1 = y1 & x2 = y2 & x3 = y3; theorem :: MCART_1:29 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]; :: :: Quadruples :: definition let x1,x2,x3,x4; func [x1,x2,x3,x4] equals :: MCART_1:def 4 [[x1,x2,x3],x4]; end; canceled; theorem :: MCART_1:31 [x1,x2,x3,x4] = [[[x1,x2],x3],x4]; theorem :: MCART_1:32 [x1,x2,x3,x4] = [[x1,x2],x3,x4]; theorem :: MCART_1:33 [x1,x2,x3,x4] = [y1,y2,y3,y4] implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4; theorem :: MCART_1:34 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]; :: :: Cartesian products of three sets :: theorem :: MCART_1:35 X1 <> {} & X2 <> {} & X3 <> {} iff [:X1,X2,X3:] <> {}; reserve xx1 for Element of X1, xx2 for Element of X2, xx3 for Element of X3; theorem :: MCART_1:36 X1<>{} & X2<>{} & X3<>{} implies ( [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies X1=Y1 & X2=Y2 & X3=Y3); theorem :: MCART_1:37 [:X1,X2,X3:]<>{} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies X1=Y1 & X2=Y2 & X3=Y3; theorem :: MCART_1:38 [:X,X,X:] = [:Y,Y,Y:] implies X = Y; theorem :: MCART_1:39 [:{x1},{x2},{x3}:] = { [x1,x2,x3] }; theorem :: MCART_1:40 [:{x1,y1},{x2},{x3}:] = { [x1,x2,x3],[y1,x2,x3] }; theorem :: MCART_1:41 [:{x1},{x2,y2},{x3}:] = { [x1,x2,x3],[x1,y2,x3] }; theorem :: MCART_1:42 [:{x1},{x2},{x3,y3}:] = { [x1,x2,x3],[x1,x2,y3] }; theorem :: MCART_1:43 [:{x1,y1},{x2,y2},{x3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3] }; theorem :: MCART_1:44 [:{x1,y1},{x2},{x3,y3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3] }; theorem :: MCART_1:45 [:{x1},{x2,y2},{x3,y3}:] = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3] }; theorem :: MCART_1:46 [:{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] }; definition let X1,X2,X3; assume X1<>{} & X2<>{} & X3<>{}; let x be Element of [:X1,X2,X3:]; func x`1 -> Element of X1 means :: MCART_1:def 5 x = [x1,x2,x3] implies it = x1; func x`2 -> Element of X2 means :: MCART_1:def 6 x = [x1,x2,x3] implies it = x2; func x`3 -> Element of X3 means :: MCART_1:def 7 x = [x1,x2,x3] implies it = x3; end; theorem :: MCART_1:47 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; theorem :: MCART_1:48 X1<>{} & X2<>{} & X3<>{} implies for x being Element of [:X1,X2,X3:] holds x = [x`1,x`2,x`3]; theorem :: MCART_1:49 X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] implies X = {}; theorem :: MCART_1:50 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; theorem :: MCART_1:51 X1<>{} & X2<>{} & X3<>{} implies for x being Element of [:X1,X2,X3:] holds x <> x`1 & x <> x`2 & x <> x`3; theorem :: MCART_1:52 [:X1,X2,X3:] meets [:Y1,Y2,Y3:] implies X1 meets Y1 & X2 meets Y2 & X3 meets Y3; :: :: Cartesian products of four sets :: theorem :: MCART_1:53 [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:]; theorem :: MCART_1:54 [:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:]; theorem :: MCART_1:55 X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} iff [:X1,X2,X3,X4:] <> {}; theorem :: MCART_1:56 X1<>{} & X2<>{} & X3<>{} & X4<>{} implies ( [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4); theorem :: MCART_1:57 [:X1,X2,X3,X4:]<>{} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4; theorem :: MCART_1:58 [:X,X,X,X:] = [:Y,Y,Y,Y:] implies X = Y; reserve xx4 for Element of X4; definition let X1,X2,X3,X4; assume X1<>{} & X2<>{} & X3<>{} & X4 <> {}; let x be Element of [:X1,X2,X3,X4:]; func x`1 -> Element of X1 means :: MCART_1:def 8 x = [x1,x2,x3,x4] implies it = x1; func x`2 -> Element of X2 means :: MCART_1:def 9 x = [x1,x2,x3,x4] implies it = x2; func x`3 -> Element of X3 means :: MCART_1:def 10 x = [x1,x2,x3,x4] implies it = x3; func x`4 -> Element of X4 means :: MCART_1:def 11 x = [x1,x2,x3,x4] implies it = x4; end; theorem :: MCART_1:59 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; theorem :: MCART_1:60 X1<>{} & X2<>{} & X3<>{} & X4<>{} implies for x being Element of [:X1,X2,X3,X4:] holds x = [x`1,x`2,x`3,x`4]; theorem :: MCART_1:61 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; theorem :: MCART_1:62 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; theorem :: MCART_1:63 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 = {}; theorem :: MCART_1:64 [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:] implies X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4; theorem :: MCART_1:65 [:{x1},{x2},{x3},{x4}:] = { [x1,x2,x3,x4] }; :: Ordered pairs theorem :: MCART_1:66 [:X,Y:] <> {} implies for x being Element of [:X,Y:] holds x <> x`1 & x <> x`2; theorem :: MCART_1:67 x in [:X,Y:] implies x <> x`1 & x <> x`2; :: 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 :: MCART_1:68 X1<>{} & X2<>{} & X3<>{} implies for x1,x2,x3 st x = [x1,x2,x3] holds x`1 = x1 & x`2 = x2 & x`3 = x3; theorem :: MCART_1:69 X1<>{} & X2<>{} & X3<>{} & (for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y1 = xx1) implies y1 =x`1; theorem :: MCART_1:70 X1<>{} & X2<>{} & X3<>{} & (for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y2 = xx2) implies y2 =x`2; theorem :: MCART_1:71 X1<>{} & X2<>{} & X3<>{} & (for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y3 = xx3) implies y3 =x`3; theorem :: MCART_1:72 z in [: X1,X2,X3 :] implies ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3]; theorem :: MCART_1:73 [x1,x2,x3] in [: X1,X2,X3 :] iff x1 in X1 & x2 in X2 & x3 in X3; theorem :: MCART_1:74 (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 :]; theorem :: MCART_1:75 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; theorem :: MCART_1:76 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; theorem :: MCART_1:77 X1 c= Y1 & X2 c= Y2 & X3 c= Y3 implies [:X1,X2,X3:] c= [:Y1,Y2,Y3:]; :: Quadruples reserve x for Element of [:X1,X2,X3,X4:]; theorem :: MCART_1:78 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; theorem :: MCART_1:79 X1<>{} & X2<>{} & X3<>{} & X4<>{} & (for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1) implies y1 =x`1; theorem :: MCART_1:80 X1<>{} & X2<>{} & X3<>{} & X4<>{} & (for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y2 = xx2) implies y2 =x`2; theorem :: MCART_1:81 X1<>{} & X2<>{} & X3<>{} & X4<>{} & (for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y3 = xx3) implies y3 =x`3; theorem :: MCART_1:82 X1<>{} & X2<>{} & X3<>{} & X4<>{} & (for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y4 = xx4) implies y4 =x`4; theorem :: MCART_1:83 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]; theorem :: MCART_1:84 [x1,x2,x3,x4] in [: X1,X2,X3,X4 :] iff x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4; theorem :: MCART_1:85 (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 :]; theorem :: MCART_1:86 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; theorem :: MCART_1:87 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; theorem :: MCART_1:88 X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 implies [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:]; definition let X1,X2,A1,A2; redefine func [:A1,A2:] -> Subset of [:X1,X2:]; end; definition let X1,X2,X3,A1,A2,A3; redefine func [:A1,A2,A3:] -> Subset of [:X1,X2,X3:]; end; definition let X1,X2,X3,X4,A1,A2,A3,A4; redefine func [:A1,A2,A3,A4:] -> Subset of [:X1,X2,X3,X4:]; end;

Back to top