:: Tuples, Projections and Cartesian Products :: by Andrzej Trybulec :: :: Received March 30, 1989 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, TARSKI, ZFMISC_1, RELAT_1, FUNCT_1, MCART_1, XTUPLE_0, RECDEF_2, FACIRC_1; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1; constructors TARSKI, ENUMSET1, XTUPLE_0, SUBSET_1, FUNCT_1; registrations RELAT_1, XTUPLE_0, SUBSET_1; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0; equalities TARSKI, XBOOLE_0, RELAT_1, XTUPLE_0; theorems TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, FUNCT_1, RELAT_1, XTUPLE_0, XREGULAR; schemes FUNCT_1; begin reserve v,x,x1,x2,x3,x4,y,y1,y2,y3,y4,z,z1,z2 for object, X,X1,X2,X3,X4,Y,Y1,Y2,Y3,Y4,Y5, Z,Z1,Z2,Z3,Z4,Z5 for set; reserve p for pair object; :: :: 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 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 XREGULAR:2; 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]; A5: { x,y } in Y by A4,TARSKI:def 2; x in { x,y } & y in { x,y } by TARSKI:def 2; hence contradiction by A2,A5,A3,XBOOLE_0:3; end; :: Now we prove theorems describing relationships between projections :: of ordered pairs and Cartesian products of two sets. theorem Th4: z in [:X,Y:] implies z`1 in X & z`2 in Y proof assume z in [:X,Y:]; then consider x,y being object such that A1: x in X & y in Y & z=[x,y] by ZFMISC_1:def 2; thus thesis by A1; end; ::\$CT theorem z in [:{x},Y:] implies z`1=x & z`2 in Y proof assume A1: z in [:{x},Y:]; then z`1 in {x} by Th4; hence thesis by A1,Th4,TARSKI:def 1; end; theorem z in [:X,{y}:] implies z`1 in X & z`2 = y proof assume A1: z in [:X,{y}:]; then z`2 in {y} by Th4; hence thesis by A1,Th4,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 Th4; 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 A1: z in [:{x1,x2},Y:]; then z`1 in {x1,x2} by Th4; hence thesis by A1,Th4,TARSKI:def 2; end; theorem z in [:X,{y1,y2}:] implies z`1 in X & (z`2 = y1 or z`2 = y2) proof assume A1: z in [:X,{y1,y2}:]; then z`2 in {y1,y2} by Th4; hence thesis by A1,Th4,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 Th4; 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 Th4; 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 Th4; hence thesis by TARSKI:def 2; end; theorem Th14: (ex y,z st x = [y,z]) implies x <> x`1 & x <> x`2 proof given y,z such that A1: x = [y,z]; now assume y = x; then {{y,z},{y}} in {y} by A1,TARSKI:def 1; hence contradiction by TARSKI:def 2; end; hence x <> x`1 by A1; now assume z = x; then {{y,z},{y}} in {y,z} by A1,TARSKI:def 2; hence contradiction by TARSKI:def 2; end; hence thesis by A1; end; :: Some of theorems proved above may be simplified , if we state them :: for elements of Cartesian product rather than for arbitrary objects. reserve R for Relation; theorem Th15: x in R implies x = [x`1,x`2] proof assume x in R; then ex x1,x2 being object st x=[x1,x2] by RELAT_1:def 1; hence thesis; 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 <> {}; let x be Element of [:X1,X2:]; reconsider xx2 = x`2 as Element of X2 by A1,Th4; reconsider xx1 = x`1 as Element of X1 by A1,Th4; take xx1,xx2; thus thesis by A1,Th15; end; registration let X1,X2 be non empty set; cluster -> pair for Element of [:X1,X2:]; coherence proof let x be Element of [:X1,X2:]; ex xx1 being Element of X1, xx2 being Element of X2 st x = [xx1,xx2] by Lm1; hence thesis; end; end; theorem X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x = [x`1,x`2] by Th15; theorem Th17: [:{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:109 .= {[x1,y1],[x1,y2]} \/ [:{x2},{y1,y2}:] by ZFMISC_1:30 .= {[x1,y1],[x1,y2]} \/ {[x2,y1],[x2,y2]} by ZFMISC_1:30 .= {[x1,y1],[x1,y2],[x2,y1],[x2,y2]} by ENUMSET1:5; end; theorem Th18: 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,Th15; hence thesis by Th14; end; :: :: Triples :: ::\$CT theorem Th19: 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 XREGULAR:4; 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 }; A5: x in Y1 & y in Y1 by TARSKI:def 2; A6: Y3 in Y by A4,TARSKI:def 2; Y1 in Y2 & Y2 in Y3 by TARSKI:def 2; hence contradiction by A2,A5,A6,A3,XBOOLE_0:3; end; :: :: Quadruples :: ::\$CT 3 theorem Th20: 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 XREGULAR:6; 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 }; A5: Y3 in Y4 & Y4 in Y5 by TARSKI:def 2; A6: Y5 in Y by A4,TARSKI:def 2; A7: x1 in Y1 & x2 in Y1 by TARSKI:def 2; Y1 in Y2 & Y2 in Y3 by TARSKI:def 2; hence contradiction by A2,A7,A5,A6,A3,XBOOLE_0:3; end; :: :: Cartesian products of three sets :: theorem Th21: X1 <> {} & X2 <> {} & X3 <> {} iff [:X1,X2,X3:] <> {} proof A1: X1 <> {} & X2 <> {} iff [:X1,X2:] <> {} by ZFMISC_1:90; [:[:X1,X2:],X3:] = [:X1,X2,X3:] by ZFMISC_1:def 3; hence thesis by A1,ZFMISC_1:90; end; reserve xx1 for Element of X1, xx2 for Element of X2, xx3 for Element of X3; theorem Th22: 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<>{}; assume A3: X3<>{}; assume [:X1,X2,X3:] = [:Y1,Y2,Y3:]; then A4: [:[:X1,X2:],X3:] = [:[:Y1,Y2:],Y3:] by A1,ZFMISC_1:def 3; then [:X1,X2:] = [:Y1,Y2:] by A2,A3,ZFMISC_1:110; hence thesis by A2,A3,A4,ZFMISC_1:110; end; theorem [:X1,X2,X3:]<>{} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies X1=Y1 & X2=Y2 & X3=Y3 proof assume A1: [:X1,X2,X3:]<>{}; then A2: X3<>{} by Th21; X1<>{} & X2<>{} by A1,Th21; hence thesis by A2,Th22; 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 Th22; hence thesis; 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 that A1: X1 <> {} & X2 <> {} and A2: X3 <> {}; let x be Element of [:X1,X2,X3:]; reconsider x9=x as Element of [:[:X1,X2:],X3:] by ZFMISC_1:def 3; consider x12 being (Element of [:X1,X2:]), xx3 such that A3: x9 = [x12,xx3] by A1,A2,Lm1; consider xx1,xx2 such that A4: x12 = [xx1,xx2] by A1,Lm1; take xx1,xx2,xx3; thus thesis by A3,A4; end; theorem Th25: [:{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:29 .= { [x1,x2,x3] } by ZFMISC_1:29; 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:30 .= { [x1,x2,x3],[y1,x2,x3] } by ZFMISC_1:30; 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:30 .= { [x1,x2,x3],[x1,y2,x3] } by ZFMISC_1:30; 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:29 .= { [x1,x2,x3],[x1,x2,y3] } by ZFMISC_1:30; 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 Th17 .= [:{[x1,x2],[x1,y2]} \/ {[y1,x2],[y1,y2]},{x3}:] by ENUMSET1:5 .= [:{[x1,x2],[x1,y2]},{x3}:] \/ [:{[y1,x2],[y1,y2]},{x3}:] by ZFMISC_1:97 .= { [[x1,x2],x3],[[x1,y2],x3]} \/ [:{[y1,x2],[y1,y2]},{x3}:] by ZFMISC_1:30 .= { [[x1,x2],x3],[[x1,y2],x3]} \/ {[[y1,x2],x3],[[y1,y2],x3] } by ZFMISC_1:30 .= { [x1,x2,x3],[x1,y2,x3],[y1,x2,x3],[[y1,y2],x3] } by ENUMSET1:5 .= { [x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3] } by ENUMSET1:62; 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:30 .= { [[x1,x2],x3],[[x1,x2],y3],[[y1,x2],x3],[[y1,x2],y3] } by Th17 .= { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3] } by ENUMSET1:62; 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:30 .= { [[x1,x2],x3],[[x1,x2],y3],[[x1,y2],x3],[[x1,y2],y3] } by Th17 .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3] } by ENUMSET1:62; 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 Th17 .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]} by ENUMSET1:62; A2: [:{[y1,x2],[y1,y2]},{x3,y3}:] = { [[y1,x2],x3],[[y1,x2],y3],[[y1,y2],x3] ,[[y1,y2],y3]} by Th17 .= { [y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3]} by ENUMSET1:62; 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 Th17 .= [:{[x1,x2],[x1,y2]} \/ {[y1,x2],[y1,y2]},{x3,y3}:] by ENUMSET1:5 .= { [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:97 .= { [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:25; end; registration let X1,X2,X3 be non empty set; cluster -> triple for Element of [:X1,X2,X3:]; coherence proof let x be Element of [:X1,X2,X3:]; ex xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 st x = [xx1,xx2,xx3] by Lm2; hence thesis; end; end; definition ::\$CD 4 let X1,X2,X3 be non empty set; let x be Element of [:X1,X2,X3:]; redefine func x`1_3 -> Element of X1 means x = [x1,x2,x3] implies it = x1; coherence proof consider xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 such that A1: x = [xx1,xx2,xx3] by Lm2; thus x`1_3 is Element of X1 by A1; end; compatibility proof let y be Element of X1; thus y = x`1_3 implies for x1,x2,x3 holds x = [x1,x2,x3] implies y = x1; assume A2: for x1,x2,x3 holds x = [x1,x2,x3] implies y = x1; consider xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 such that A3: x = [xx1,xx2,xx3] by Lm2; thus y = x`1_3 by A2,A3; end; redefine func x`2_3 -> Element of X2 means x = [x1,x2,x3] implies it = x2; coherence proof consider xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 such that A4: x = [xx1,xx2,xx3] by Lm2; thus x`2_3 is Element of X2 by A4; end; compatibility proof let y be Element of X2; thus y = x`2_3 implies for x1,x2,x3 holds x = [x1,x2,x3] implies y = x2; assume A5: for x1,x2,x3 holds x = [x1,x2,x3] implies y = x2; consider xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 such that A6: x = [xx1,xx2,xx3] by Lm2; thus y = x`2_3 by A5,A6; end; redefine func x`3_3 -> Element of X3 means x = [x1,x2,x3] implies it = x3; coherence proof consider xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 such that A7: x = [xx1,xx2,xx3] by Lm2; thus x`3_3 is Element of X3 by A7; end; compatibility proof let y be Element of X3; thus y = x`3_3 implies for x1,x2,x3 holds x = [x1,x2,x3] implies y = x3; assume A8: for x1,x2,x3 holds x = [x1,x2,x3] implies y = x3; consider xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 such that A9: x = [xx1,xx2,xx3] by Lm2; thus y = x`3_3 by A8,A9; end; end; ::\$CT 2 theorem Th34: 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; then reconsider X,Y,Z as non empty set by Th21; per cases by A1; suppose A3: X c= [:X,Y,Z:]; consider v such that A4: v in X and A5: for x,y,z st x in X or y in X holds v <> [x,y,z] by Th19; reconsider v as Element of [:X,Y,Z:] by A3,A4; v = [v`1_3,v`2_3,v`3_3]; hence contradiction by A5; end; suppose X c= [:Y,Z,X:]; then X c= [:[:Y,Z:],X:] by ZFMISC_1:def 3; hence thesis by ZFMISC_1:111; end; suppose A6: X c= [:Z,X,Y:]; consider v such that A7: v in X and A8: for z,x,y st z in X or x in X holds v <> [z,x,y] by Th19; reconsider v as Element of [:Z,X,Y:] by A6,A7; v = [v`1_3,v`2_3,v`3_3]; hence thesis by A8; end; end; ::\$CT theorem Th35: 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 proof let X1,X2,X3 be non empty set; let x be Element of [:X1,X2,X3:]; set Y9 = { x`1_3,x`2_3 }, Y = { Y9,{x`1_3}}, X9 = { Y,x`3_3 }, X = { X9,{Y} }; A1: x = [x`1_3,x`2_3,x`3_3] .= [[x`1_3,x`2_3],x`3_3]; then x = x`1_3 or x = x`2_3 implies X in Y9 & Y9 in Y & Y in X9 & X9 in X by TARSKI:def 2; hence x <> x`1_3 & x <> x`2_3 by XREGULAR:8; thus thesis by A1,Th14; end; theorem [:X1,X2,X3:] meets [:Y1,Y2,Y3:] implies X1 meets Y1 & X2 meets Y2 & X3 meets Y3 proof assume A1: [:X1,X2,X3:] meets [:Y1,Y2,Y3:]; A2: [:[:X1,X2:],X3:] = [:X1,X2,X3:] & [:[:Y1,Y2:],Y3:] = [:Y1,Y2,Y3:] by ZFMISC_1:def 3; then [:X1,X2:] meets [:Y1,Y2:] by A1,ZFMISC_1:104; hence thesis by A2,A1,ZFMISC_1:104; end; :: :: Cartesian products of four sets :: theorem Th37: [: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 Th38: [:[: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 Th37; end; theorem Th39: 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 Th21; hence thesis by A1,ZFMISC_1:90; end; theorem Th40: X1<>{} & X2<>{} & X3<>{} & X4<>{} & [: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<>{}; assume A3: X4<>{}; assume [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:]; then A4: [:[:X1,X2,X3:],X4:] = [:[:Y1,Y2,Y3:],Y4:] by A1,ZFMISC_1:def 4; [:X1,X2,X3:] = [:Y1,Y2,Y3:] by A3,A4,A2,ZFMISC_1:110; hence thesis by A2,A3,A4,Th22,ZFMISC_1:110; 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 A1: [:X1,X2,X3,X4:]<>{}; then A2: X3<>{} & X4<>{} by Th39; X1<>{} & X2<>{} by A1,Th39; hence thesis by A2,Th40; 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 Th40; hence thesis; 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 that A1: X1 <> {} & X2 <> {} & X3 <> {} and A2: X4 <> {}; let x be Element of [:X1,X2,X3,X4:]; reconsider x9=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: x9 = [x123,xx4] by A2,Lm1,A1; consider xx1,xx2,xx3 such that A4: x123 = [xx1,xx2,xx3] by A1,Lm2; take xx1,xx2,xx3,xx4; thus thesis by A3,A4; end; registration let X1,X2,X3,X4 be non empty set; cluster -> quadruple for Element of [:X1,X2,X3,X4:]; coherence proof let x be Element of [:X1,X2,X3,X4:]; ex xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] by Lm3; hence thesis; end; end; definition let X1,X2,X3,X4 be non empty set; let x be Element of [:X1,X2,X3,X4:]; redefine func x`1_4 -> Element of X1 means x = [x1,x2,x3,x4] implies it = x1; coherence proof consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that A1: x = [xx1,xx2,xx3,xx4] by Lm3; thus x`1_4 is Element of X1 by A1; end; compatibility proof let y be Element of X1; thus y = x`1_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x1; assume A2: for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x1; consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that A3: x = [xx1,xx2,xx3,xx4] by Lm3; thus y = x`1_4 by A2,A3; end; redefine func x`2_4 -> Element of X2 means x = [x1,x2,x3,x4] implies it = x2; coherence proof consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that A4: x = [xx1,xx2,xx3,xx4] by Lm3; thus x`2_4 is Element of X2 by A4; end; compatibility proof let y be Element of X2; thus y = x`2_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x2; assume A5: for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x2; consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that A6: x = [xx1,xx2,xx3,xx4] by Lm3; thus y = x`2_4 by A5,A6; end; redefine func x`3_4 -> Element of X3 means x = [x1,x2,x3,x4] implies it = x3; coherence proof consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that A7: x = [xx1,xx2,xx3,xx4] by Lm3; thus x`3_4 is Element of X3 by A7; end; compatibility proof let y be Element of X3; thus y = x`3_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x3; assume A8: for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x3; consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that A9: x = [xx1,xx2,xx3,xx4] by Lm3; thus y = x`3_4 by A8,A9; end; redefine func x`4_4 -> Element of X4 means x = [x1,x2,x3,x4] implies it = x4; coherence proof consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that A10: x = [xx1,xx2,xx3,xx4] by Lm3; thus x`4_4 is Element of X4 by A10; end; compatibility proof let y be Element of X4; thus y = x`4_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x4; assume A11: for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x4; consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that A12: x = [xx1,xx2,xx3,xx4] by Lm3; thus y = x`4_4 by A11,A12; end; end; ::\$CT 3 theorem 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 proof let X1,X2,X3,X4 be non empty set; let x be Element of [:X1,X2,X3,X4:]; reconsider Y = [:X1,X2:], X3, X4 as non empty set; reconsider x9=x as Element of [:Y,X3,X4:] by Th38; set Z9 = { x`1_4,x`2_4 }, Z = { Z9,{x`1_4}}, Y9 = { Z,x`3_4 }, Y = { Y9,{Z} }, X9 = { Y,x`4_4 }, X = { X9,{Y} }; x = [x`1_4,x`2_4,x`3_4,x`4_4] .= X; then x = x`1_4 or x = x`2_4 implies X in Z9 & Z9 in Z & Z in Y9 & Y9 in Y & Y in X9 & X9 in X by TARSKI:def 2; hence x <> x`1_4 & x <> x`2_4 by XREGULAR:10; x`3_4 = (x qua set)`1`2 .= x9`2_3; hence thesis by Th35; 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 <> {}; A3: [:X1,X2,X3,X4:]<>{} or [:X2,X3,X4,X1:]<>{} or [:X3,X4,X1,X2:]<>{} or [: X4,X1,X2,X3:]<>{} by A1,A2; reconsider X1,X2,X3,X4 as non empty set by A3,Th39; 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 Th20; reconsider v as Element of [:X1,X2,X3,X4:] by A4,A5; v = [v`1_4,v`2_4,v`3_4,v`4_4]; hence contradiction by A6; end; suppose X1 c= [:X2,X3,X4,X1:]; then X1 c= [:[:X2,X3:],X4,X1:] by Th38; hence thesis by Th34; end; suppose X1 c= [:X3,X4,X1,X2:]; then X1 c= [:[:X3,X4:],X1,X2:] by Th38; hence thesis by Th34; end; 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 Th20; reconsider v as Element of [:X4,X1,X2,X3:] by A7,A8; v = [v`1_4,v`2_4,v`3_4,v`4_4]; hence thesis by A9; end; 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 assume A1: [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:]; A2: [:[:[:X1,X2:],X3:],X4:] = [:X1,X2,X3,X4:] & [:[:[:Y1,Y2:],Y3:],Y4:] = [: Y1, Y2,Y3,Y4:] by Th37; then A3: [:[:X1,X2:],X3:] meets [:[:Y1,Y2:],Y3:] by A1,ZFMISC_1:104; then [:X1,X2:] meets [:Y1,Y2:] by ZFMISC_1:104; hence thesis by A2,A1,A3,ZFMISC_1:104; end; theorem [:{x1},{x2},{x3},{x4}:] = { [x1,x2,x3,x4] } proof thus [:{x1},{x2},{x3},{x4}:] = [:[:{x1},{x2}:],{x3},{x4}:] by Th38 .= [:{[x1,x2]},{x3},{x4}:] by ZFMISC_1:29 .= {[[x1,x2],x3,x4]} by Th25 .= { [x1,x2,x3,x4] }; end; :: Ordered pairs theorem Th48: [: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:90; hence thesis by Th18; end; theorem x in [:X,Y:] implies x <> x`1 & x <> x`2 by Th48; :: 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 for X1,X2,X3 being non empty set for x being Element of [:X1,X2,X3:] for x1,x2,x3 st x = [x1,x2,x3] holds x`1_3 = x1 & x`2_3 = x2 & x`3_3 = x3; theorem for X1,X2,X3 being non empty set for x being Element of [:X1,X2,X3:] st for xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y1 = xx1 holds y1 =x`1_3 proof let X1,X2,X3 be non empty set; let x be Element of [:X1,X2,X3:]; assume that A1: for xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y1 = xx1; x = [x`1_3,x`2_3,x`3_3]; hence thesis by A1; end; theorem for X1,X2,X3 being non empty set for x being Element of [:X1,X2,X3:] st for xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y2 = xx2 holds y2 =x`2_3 proof let X1,X2,X3 be non empty set; let x be Element of [:X1,X2,X3:]; assume that A1: for xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y2 = xx2; x = [x`1_3,x`2_3,x`3_3]; hence thesis by A1; end; theorem for X1,X2,X3 being non empty set for x being Element of [:X1,X2,X3:] st for xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y3 = xx3 holds y3 =x`3_3 proof let X1,X2,X3 be non empty set; let x be Element of [:X1,X2,X3:]; assume that A1: for xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y3 = xx3; x = [x`1_3,x`2_3,x`3_3]; hence thesis by A1; end; theorem Th54: 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 object 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 object such that A4: x1 in X1 & x2 in X2 and A5: x12 = [x1,x2] by A1,ZFMISC_1:def 2; z = [x1,x2,x3] by A3,A5; hence thesis by A2,A4; end; theorem Th55: [x1,x2,x3] in [: X1,X2,X3 :] iff x1 in X1 & x2 in X2 & x3 in X3 proof A1: [x1,x2] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:87; [:X1,X2,X3:] = [:[:X1,X2:],X3:] by ZFMISC_1:def 3; hence thesis by A1,ZFMISC_1:87; 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 be object; 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 and A3: x3 in X3 & z = [x1,x2,x3] by A1; [x1,x2] in [:X1,X2:] by A2,ZFMISC_1:def 2; hence thesis by A3,ZFMISC_1:def 2; end; assume z in [:[:X1,X2:],X3:]; then consider x12,x3 being object 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 object such that A7: x1 in X1 & x2 in X2 and A8: x12 = [x1,x2] by A4,ZFMISC_1:def 2; z = [x1,x2,x3] by A6,A8; hence z in Z by A1,A5,A7; end; then Z = [:[:X1,X2:],X3:] by TARSKI:2; hence thesis by ZFMISC_1:def 3; end; ::\$CT theorem for X1,X2,X3 being non empty set for A1 being non empty Subset of X1, A2 being non empty Subset of X2, 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 let X1,X2,X3 be non empty set; let A1 be non empty Subset of X1, A2 be non empty Subset of X2, A3 be non empty Subset of X3; let x be Element of [:X1,X2,X3:]; assume x in [:A1,A2,A3:]; then reconsider y = x as Element of [:A1,A2,A3:]; A1: y`2_3 in A2; A2: y`3_3 in A3; y`1_3 in A1; hence thesis by A1,A2; end; theorem Th58: X1 c= Y1 & X2 c= Y2 & X3 c= Y3 implies [:X1,X2,X3:] c= [:Y1,Y2, Y3:] proof A1: [:X1,X2,X3:] = [:[:X1,X2:],X3:] & [:Y1,Y2,Y3:] = [:[:Y1,Y2:],Y3:] by ZFMISC_1:def 3; assume X1 c= Y1 & X2 c= Y2; then A2: [:X1,X2:] c= [:Y1,Y2:] by ZFMISC_1:96; assume X3 c= Y3; hence thesis by A2,A1,ZFMISC_1:96; end; :: Quadruples reserve x for Element of [:X1,X2,X3,X4:]; theorem for X1,X2,X3,X4 being non empty set for x being Element of [:X1,X2,X3,X4:] for x1,x2,x3,x4 being set st x = [x1, x2,x3,x4] holds x`1_4 = x1 & x`2_4 = x2 & x`3_4 = x3 & x`4_4 = x4; theorem 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, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1 holds y1 =x`1_4 proof let X1,X2,X3,X4 be non empty set; let x be Element of [:X1,X2,X3,X4:]; assume that A1: for xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1; x = [x`1_4,x`2_4,x`3_4,x`4_4]; hence thesis by A1; end; theorem 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, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1, xx2,xx3,xx4] holds y2 = xx2 holds y2 =x`2_4 proof let X1,X2,X3,X4 be non empty set; let x be Element of [:X1,X2,X3,X4:]; assume that A1: for xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y2 = xx2; x = [x`1_4,x`2_4,x`3_4,x`4_4]; hence thesis by A1; end; theorem 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, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1, xx2,xx3,xx4] holds y3 = xx3 holds y3 =x`3_4 proof let X1,X2,X3,X4 be non empty set; let x be Element of [:X1,X2,X3,X4:]; assume that A1: for xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y3 = xx3; x = [x`1_4,x`2_4,x`3_4,x`4_4]; hence thesis by A1; end; theorem 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, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1, xx2,xx3,xx4] holds y4 = xx4 holds y4 =x`4_4 proof let X1,X2,X3,X4 be non empty set; let x be Element of [:X1,X2,X3,X4:]; assume that A1: for xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y4 = xx4; x = [x`1_4,x`2_4,x`3_4,x`4_4]; hence thesis by A1; 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 object 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 and A5: x123 = [x1,x2,x3] by A1,Th54; z = [x1,x2,x3,x4] by A3,A5; 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] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:87; [:X1,X2,X3,X4:] = [:[:X1,X2:],X3,X4:] & [x1,x2,x3,x4] = [[x1,x2],x3,x4] by Th38; hence thesis by A1,Th55; 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 be object; 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 and A3: x4 in X4 & z = [x1,x2,x3,x4] by A1; [x1,x2,x3] in [:X1,X2,X3:] by A2,Th55; hence thesis by A3,ZFMISC_1:def 2; end; assume z in [:[:X1,X2,X3:],X4:]; then consider x123,x4 being object 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 and A8: x123 = [x1,x2,x3] by A4,Th54; z = [x1,x2,x3,x4] by A6,A8; hence z in Z by A1,A5,A7; end; then Z = [:[:X1,X2,X3:],X4:] by TARSKI:2; hence thesis by ZFMISC_1:def 4; end; ::\$CT theorem for X1,X2,X3,X4 being non empty set, A1 being non empty Subset of X1, A2 being non empty Subset of X2, A3 being non empty Subset of X3, 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 let X1,X2,X3,X4 be non empty set, A1 be non empty Subset of X1, A2 be non empty Subset of X2, A3 be non empty Subset of X3, A4 be non empty Subset of X4; let x be Element of [:X1,X2,X3,X4:]; assume x in [:A1,A2,A3,A4:]; then reconsider y = x as Element of [:A1,A2,A3,A4:]; A1: y`2_4 in A2; A2: y`4_4 in A4; A3: y`3_4 in A3; y`1_4 in A1; hence thesis by A1,A3,A2; end; theorem Th68: X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 implies [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:] proof A1: [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] & [:Y1,Y2,Y3,Y4:] = [:[:Y1,Y2,Y3:] ,Y4 :] by ZFMISC_1:def 4; assume X1 c= Y1 & X2 c= Y2 & X3 c= Y3; then A2: [:X1,X2,X3:] c= [:Y1,Y2,Y3:] by Th58; assume X4 c= Y4; hence thesis by A2,A1,ZFMISC_1:96; end; definition let X1,X2,A1,A2; redefine func [:A1,A2:] -> Subset of [:X1,X2:]; coherence by ZFMISC_1:96; end; definition let X1,X2,X3,A1,A2,A3; redefine func [:A1,A2,A3:] -> Subset of [:X1,X2,X3:]; coherence by Th58; 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 Th68; end; begin :: Addenda :: from DTCONSTR definition let f be Function; func pr1 f -> Function means dom it = dom f & for x being object st x in dom f holds it.x = (f.x)`1; existence proof deffunc F(object) = (f.\$1)`1; ex g being Function st dom g = dom f & for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let p1, p2 be Function such that A1: dom p1 = dom f and A2: for x being object st x in dom f holds p1.x = (f.x)`1 and A3: dom p2 = dom f and A4: for x being object st x in dom f holds p2.x = (f.x)`1; now let x be object; assume A5: x in dom f; then p1.x = (f.x)`1 by A2; hence p1.x = p2.x by A4,A5; end; hence thesis by A1,A3,FUNCT_1:2; end; func pr2 f -> Function means dom it = dom f & for x being object st x in dom f holds it.x = (f.x)`2; existence proof deffunc F(object) = (f.\$1)`2; ex g being Function st dom g = dom f & for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let p1, p2 be Function such that A6: dom p1 = dom f and A7: for x being object st x in dom f holds p1.x = (f.x)`2 and A8: dom p2 = dom f and A9: for x being object st x in dom f holds p2.x = (f.x)`2; now let x be object; assume A10: x in dom f; then p1.x = (f.x)`2 by A7; hence p1.x = p2.x by A9,A10; end; hence thesis by A6,A8,FUNCT_1:2; end; end; definition let x be object; func x`11 -> set equals x`1`1; coherence by TARSKI:1; func x`12 -> set equals x`1`2; coherence by TARSKI:1; func x`21 -> set equals x`2`1; coherence by TARSKI:1; func x`22 -> set equals x`2`2; coherence by TARSKI:1; end; reserve x for object; theorem [[x1,x2],y]`11 = x1 & [[x1,x2],y]`12 = x2 & [x,[y1,y2]]`21 = y1 & [x,[ y1,y2]]`22 = y2; :: missing, 2007.04.13, A.T. theorem x in R implies x`1 in dom R & x`2 in rng R proof assume A1: x in R; then x = [x`1,x`2] by Th15; hence thesis by A1,XTUPLE_0:def 12,def 13; end; :: 2009.08.29, A.T. theorem Th71: for R being non empty Relation, x being object holds Im(R,x) = { I`2 where I is Element of R: I`1 = x } proof let R be non empty Relation, x being object; set X = { I`2 where I is Element of R: I`1 = x }; thus Im(R,x) c= X proof let z be object; assume z in Im(R,x); then consider y being object such that A1: [y,z] in R and A2: y in {x} by RELAT_1:def 13; A3: y = x by A2,TARSKI:def 1; y = [y,z]`1 & z = [y,z]`2; hence z in X by A1,A3; end; let z be object; assume z in X; then consider I being Element of R such that A4: z= I`2 and A5: I`1 = x; A6: I = [I`1,I`2] by Th15; x in {x} by TARSKI:def 1; hence z in Im(R,x) by A4,A5,A6,RELAT_1:def 13; end; theorem x in R implies x`2 in Im(R,x`1) proof assume A1: x in R; then x`2 in { I`2 where I is Element of R: I`1 = x`1 }; hence thesis by A1,Th71; end; theorem Th73: x in R & y in R & x`1 = y`1 & x`2 = y`2 implies x = y proof assume x in R & y in R; then x = [x`1,x`2] & y = [y`1,y`2] by Th15; hence thesis; end; theorem for R being non empty Relation, x,y being Element of R st x`1 = y`1 & x`2 = y`2 holds x = y by Th73; :: 2010.05.120, A.T. theorem proj1 proj1 {[x1,x2,x3],[y1,y2,y3]} = {x1,y1} proof thus proj1 proj1 {[x1,x2,x3],[y1,y2,y3]} = proj1 {[x1,x2],[y1,y2]} by RELAT_1:10 .= {x1,y1} by RELAT_1:10; end; theorem proj1 proj1 {[x1,x2,x3]} = {x1} proof thus proj1 proj1 {[x1,x2,x3]} = proj1 {[x1,x2]} by RELAT_1:9 .= {x1} by RELAT_1:9; end; scheme BiFuncEx{A()->set,B()->set,C()->set,P[object,object,object]}: ex f,g being Function st dom f = A() & dom g = A() & for x st x in A() holds P[x,f.x,g.x] provided A1: x in A() implies ex y,z st y in B() & z in C() & P[x,y,z]; defpred H[object,object] means for y,z st \$2`1 = y & \$2`2 = z holds P[\$1,y,z]; A2: for x being object st x in A() ex p being object st p in [:B(),C():] & H[x,p] proof let x be object; assume x in A(); then consider y,z such that A3: y in B() & z in C() and A4: P[x,y,z] by A1; reconsider p=[y,z] as set; take p; thus p in [:B(),C():] by A3,ZFMISC_1:87; thus for y,z st p`1 = y & p`2 = z holds P[x,y,z] by A4; end; consider h being Function such that dom h = A() & rng h c= [:B(),C():] and A5: for x being object st x in A() holds H[x,h.x] from FUNCT_1:sch 6(A2); deffunc g(object) = (h.\$1)`2; deffunc f(object) = (h.\$1)`1; consider f being Function such that A6: dom f = A() and A7: for x being object st x in A() holds f.x = f(x) from FUNCT_1:sch 3; consider g being Function such that A8: dom g = A() and A9: for x being object st x in A() holds g.x = g(x) from FUNCT_1:sch 3; take f,g; thus dom f = A() & dom g = A() by A6,A8; thus for x st x in A() holds P[x,f.x,g.x] proof let x; assume A10: x in A(); then f.x = (h.x)`1 & g.x = (h.x)`2 by A7,A9; hence thesis by A5,A10; end; end; theorem [[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] = [y1,y2] & [x3,x4] = [y3,y4] by XTUPLE_0:1; hence x1=y1 & x2=y2 & x3=y3 & x4=y4 by XTUPLE_0:1; end;