Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Domains and Their Cartesian Products

**by****Andrzej Trybulec**- Received April 3, 1989
- MML identifier: DOMAIN_1

- [ Mizar article, MML identifier index ]

environ vocabulary SUBSET_1, MCART_1, BOOLE; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, MCART_1; constructors TARSKI, ENUMSET1, MCART_1, XBOOLE_0; clusters SUBSET_1, XBOOLE_0, ZFMISC_1; requirements SUBSET, BOOLE; begin reserve a,b,c,d for set; reserve D,X1,X2,X3,X4 for non empty set; reserve x1,y1,z1 for Element of X1, x2 for Element of X2, x3 for Element of X3, x4 for Element of X4; reserve A1,B1 for Subset of X1; ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: :: Domains and their elements :: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: canceled 8; theorem :: DOMAIN_1:9 a in [:X1,X2:] implies ex x1,x2 st a=[x1,x2]; canceled 2; theorem :: DOMAIN_1:12 for x,y being Element of [:X1,X2:] st x`1=y`1 & x`2=y`2 holds x=y; definition let X1,X2,x1,x2; redefine func [x1,x2] -> Element of [:X1,X2:]; end; definition let X1,X2; let x be Element of [:X1,X2:]; redefine func x`1 -> Element of X1; redefine func x`2 -> Element of X2; end; ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: :: Cartesian products of three sets :: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: canceled 2; theorem :: DOMAIN_1:15 a in [: X1,X2,X3 :] iff ex x1,x2,x3 st a = [x1,x2,x3]; theorem :: DOMAIN_1:16 (for a holds a in D iff ex x1,x2,x3 st a = [x1,x2,x3]) implies D = [: X1,X2,X3 :]; theorem :: DOMAIN_1:17 D = [: X1,X2,X3 :] iff for a holds a in D iff ex x1,x2,x3 st a = [x1,x2,x3]; reserve x,y for Element of [:X1,X2,X3:]; definition let X1,X2,X3,x1,x2,x3; redefine func [x1,x2,x3] -> Element of [:X1,X2,X3:]; end; canceled 6; theorem :: DOMAIN_1:24 a =x`1 iff for x1,x2,x3 st x = [x1,x2,x3] holds a = x1; theorem :: DOMAIN_1:25 b =x`2 iff for x1,x2,x3 st x = [x1,x2,x3] holds b = x2; theorem :: DOMAIN_1:26 c =x`3 iff for x1,x2,x3 st x = [x1,x2,x3] holds c = x3; canceled; theorem :: DOMAIN_1:28 x`1=y`1 & x`2=y`2 & x`3=y`3 implies x=y; canceled 2; theorem :: DOMAIN_1:31 a in [: X1,X2,X3,X4 :] iff ex x1,x2,x3,x4 st a = [x1,x2,x3,x4]; theorem :: DOMAIN_1:32 (for a holds a in D iff ex x1,x2,x3,x4 st a = [x1,x2,x3,x4]) implies D = [: X1,X2,X3,X4 :]; theorem :: DOMAIN_1:33 D = [: X1,X2,X3,X4 :] iff for a holds a in D iff ex x1,x2,x3,x4 st a = [x1,x2,x3,x4]; reserve x for Element of [:X1,X2,X3,X4:]; definition let X1,X2,X3,X4,x1,x2,x3,x4; redefine func [x1,x2,x3,x4] -> Element of [:X1,X2,X3,X4:]; end; canceled 6; theorem :: DOMAIN_1:40 a=x`1 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds a = x1; theorem :: DOMAIN_1:41 b=x`2 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds b = x2; theorem :: DOMAIN_1:42 c = x`3 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds c = x3; theorem :: DOMAIN_1:43 d=x`4 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds d = x4; canceled; theorem :: DOMAIN_1:45 for x,y being Element of [:X1,X2,X3,X4:] st x`1=y`1 & x`2=y`2 & x`3=y`3 & x`4=y`4 holds x=y; reserve A2 for Subset of X2, A3 for Subset of X3, A4 for Subset of X4; scheme Fraenkel1 {P[set]}: for X1 holds { x1 : P[x1] } is Subset of X1; scheme Fraenkel2 {P[set,set]}: for X1,X2 holds { [x1,x2] : P[x1,x2] } is Subset of [:X1,X2:]; scheme Fraenkel3 {P[set,set,set]}: for X1,X2,X3 holds { [x1,x2,x3] : P[x1,x2,x3] } is Subset of [:X1,X2,X3:]; scheme Fraenkel4 {P[set,set,set,set]}: for X1,X2,X3,X4 holds { [x1,x2,x3,x4] : P[x1,x2,x3,x4] } is Subset of [:X1,X2,X3,X4:]; scheme Fraenkel5 {P[set],Q[set]}: for X1 st for x1 holds P[x1] implies Q[x1] holds { y1 : P[y1] } c= { z1 : Q[z1] }; scheme Fraenkel6 {P[set],Q[set]}: for X1 st for x1 holds P[x1] iff Q[x1] holds { y1 : P[y1] } = { z1 : Q[z1] }; scheme SubsetD{D() -> non empty set,P[set]}: {d where d is Element of D() : P[d]} is Subset of D(); canceled 2; theorem :: DOMAIN_1:48 X1 = { x1 : not contradiction }; theorem :: DOMAIN_1:49 [:X1,X2:] = { [x1,x2] : not contradiction }; theorem :: DOMAIN_1:50 [:X1,X2,X3:] = { [x1,x2,x3] : not contradiction }; theorem :: DOMAIN_1:51 [:X1,X2,X3,X4:] = { [x1,x2,x3,x4] : not contradiction }; theorem :: DOMAIN_1:52 A1 = { x1 : x1 in A1 }; theorem :: DOMAIN_1:53 [:A1,A2:] = { [x1,x2] : x1 in A1 & x2 in A2 }; theorem :: DOMAIN_1:54 [:A1,A2,A3:] = { [x1,x2,x3] : x1 in A1 & x2 in A2 & x3 in A3 }; theorem :: DOMAIN_1:55 [:A1,A2,A3,A4:] = { [x1,x2,x3,x4] : x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 }; theorem :: DOMAIN_1:56 {} X1 = { x1 : contradiction }; theorem :: DOMAIN_1:57 A1` = { x1 : not x1 in A1 }; theorem :: DOMAIN_1:58 A1 /\ B1 = { x1 : x1 in A1 & x1 in B1 }; theorem :: DOMAIN_1:59 A1 \/ B1 = { x1 : x1 in A1 or x1 in B1 }; theorem :: DOMAIN_1:60 A1 \ B1 = { x1 : x1 in A1 & not x1 in B1 }; theorem :: DOMAIN_1:61 A1 \+\ B1 = { x1 : x1 in A1 & not x1 in B1 or not x1 in A1 & x1 in B1 }; theorem :: DOMAIN_1:62 A1 \+\ B1 = { x1 : not x1 in A1 iff x1 in B1 }; theorem :: DOMAIN_1:63 A1 \+\ B1 = { x1 : x1 in A1 iff not x1 in B1 }; theorem :: DOMAIN_1:64 A1 \+\ B1 = { x1 : not(x1 in A1 iff x1 in B1) }; definition let D be non empty set; let x1 be Element of D; redefine func {x1} -> Subset of D; let x2 be Element of D; redefine func {x1,x2} -> Subset of D; let x3 be Element of D; redefine func {x1,x2,x3} -> Subset of D; let x4 be Element of D; redefine func {x1,x2,x3,x4} -> Subset of D; let x5 be Element of D; redefine func {x1,x2,x3,x4,x5} -> Subset of D; let x6 be Element of D; redefine func {x1,x2,x3,x4,x5,x6} -> Subset of D; let x7 be Element of D; redefine func {x1,x2,x3,x4,x5,x6,x7} -> Subset of D; let x8 be Element of D; redefine func {x1,x2,x3,x4,x5,x6,x7,x8} -> Subset of D; end;

Back to top