Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Some Basic Properties of Sets

**by****Czeslaw Bylinski**- Received February 1, 1989
- MML identifier: ZFMISC_1

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, TARSKI, ZFMISC_1; notation TARSKI, XBOOLE_0; constructors TARSKI, XBOOLE_0; clusters XBOOLE_0; begin reserve v,x,x1,x2,y,y1,y2,z,A,B,X,X1,X2,X3,X4,Y,Y1,Y2,Z,N,M for set; definition let x, y be set; cluster [x,y] -> non empty; end; definition let X; func bool X means :: ZFMISC_1:def 1 Z in it iff Z c= X; end; definition let X1,X2; func [: X1,X2 :] means :: ZFMISC_1:def 2 z in it iff ex x,y st x in X1 & y in X2 & z = [x,y]; end; definition let X1,X2,X3; func [: X1,X2,X3 :] equals :: ZFMISC_1:def 3 [:[:X1,X2:],X3:]; end; definition let X1,X2,X3,X4; func [: X1,X2,X3,X4 :] equals :: ZFMISC_1:def 4 [:[:X1,X2,X3:],X4:]; end; begin :: :: Empty set. :: theorem :: ZFMISC_1:1 bool {} = { {} }; theorem :: ZFMISC_1:2 union {} = {}; :: :: Singleton and unordered pairs. :: canceled 3; theorem :: ZFMISC_1:6 {x} c= {y} implies x = y; canceled; theorem :: ZFMISC_1:8 {x} = {y1,y2} implies x = y1; theorem :: ZFMISC_1:9 {x} = {y1,y2} implies y1 = y2; theorem :: ZFMISC_1:10 { x1,x2 } = { y1,y2 } implies x1 = y1 or x1 = y2; canceled; theorem :: ZFMISC_1:12 {x} c= {x,y}; theorem :: ZFMISC_1:13 {x} \/ {y} = {x} implies x = y; theorem :: ZFMISC_1:14 {x} \/ {x,y} = {x,y}; canceled; theorem :: ZFMISC_1:16 {x} misses {y} implies x <> y; theorem :: ZFMISC_1:17 x <> y implies {x} misses {y}; theorem :: ZFMISC_1:18 {x} /\ {y} = {x} implies x = y; theorem :: ZFMISC_1:19 {x} /\ {x,y} = {x}; theorem :: ZFMISC_1:20 {x} \ {y} = {x} iff x <> y; theorem :: ZFMISC_1:21 {x} \ {y} = {} implies x = y; theorem :: ZFMISC_1:22 {x} \ {x,y} = {}; theorem :: ZFMISC_1:23 x <> y implies { x,y } \ { y } = { x }; theorem :: ZFMISC_1:24 {x} c= {y} implies x = y; theorem :: ZFMISC_1:25 {z} c= {x,y} implies z = x or z = y; theorem :: ZFMISC_1:26 {x,y} c= {z} implies x = z; theorem :: ZFMISC_1:27 {x,y} c= {z} implies {x,y} = {z}; theorem :: ZFMISC_1:28 {x1,x2} c= {y1,y2} implies x1 = y1 or x1 = y2; theorem :: ZFMISC_1:29 x <> y implies { x } \+\ { y } = { x,y }; theorem :: ZFMISC_1:30 bool { x } = { {} , { x }}; theorem :: ZFMISC_1:31 union { x } = x; theorem :: ZFMISC_1:32 union {{x},{y}} = {x,y}; :: :: Ordered pairs. :: theorem :: ZFMISC_1:33 [x1,x2] = [y1,y2] implies x1 = y1 & x2 = y2; theorem :: ZFMISC_1:34 [x,y] in [:{x1},{y1}:] iff x = x1 & y = y1; theorem :: ZFMISC_1:35 [:{x},{y}:] = {[x,y]}; theorem :: ZFMISC_1:36 [:{x},{y,z}:] = {[x,y],[x,z]} & [:{x,y},{z}:] = {[x,z],[y,z]}; :: :: Singleton and unordered pairs included in a set. :: theorem :: ZFMISC_1:37 {x} c= X iff x in X; theorem :: ZFMISC_1:38 {x1,x2} c= Z iff x1 in Z & x2 in Z; :: :: Set included in a singleton (or unordered pair). :: theorem :: ZFMISC_1:39 Y c= { x } iff Y = {} or Y = { x }; theorem :: ZFMISC_1:40 Y c= X & not x in Y implies Y c= X \ { x }; theorem :: ZFMISC_1:41 X <> {x} & X <> {} implies ex y st y in X & y <> x; theorem :: ZFMISC_1:42 Z c= {x1,x2} iff Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2}; :: :: Sum of an unordered pair (or a singleton) and a set. :: theorem :: ZFMISC_1:43 {z} = X \/ Y implies X = {z} & Y = {z} or X = {} & Y = {z} or X = {z} & Y = {}; theorem :: ZFMISC_1:44 {z} = X \/ Y & X <> Y implies X = {} or Y = {}; theorem :: ZFMISC_1:45 {x} \/ X c= X implies x in X; theorem :: ZFMISC_1:46 x in X implies {x} \/ X = X; theorem :: ZFMISC_1:47 {x,y} \/ Z c= Z implies x in Z; theorem :: ZFMISC_1:48 x in Z & y in Z implies {x,y} \/ Z = Z; theorem :: ZFMISC_1:49 {x} \/ X <> {}; theorem :: ZFMISC_1:50 {x,y} \/ X <> {}; :: :: Intersection of an unordered pair (or a singleton) and a set. :: theorem :: ZFMISC_1:51 X /\ {x} = {x} implies x in X; theorem :: ZFMISC_1:52 x in X implies X /\ {x} = {x}; theorem :: ZFMISC_1:53 x in Z & y in Z implies {x,y} /\ Z = {x,y}; theorem :: ZFMISC_1:54 {x} misses X implies not x in X; theorem :: ZFMISC_1:55 {x,y} misses Z implies not x in Z; theorem :: ZFMISC_1:56 not x in X implies {x} misses X; theorem :: ZFMISC_1:57 not x in Z & not y in Z implies {x,y} misses Z; theorem :: ZFMISC_1:58 {x} misses X or {x} /\ X = {x}; theorem :: ZFMISC_1:59 {x,y} /\ X = {x} implies not y in X or x = y; theorem :: ZFMISC_1:60 x in X & (not y in X or x = y) implies {x,y} /\ X = {x}; canceled 2; theorem :: ZFMISC_1:63 {x,y} /\ X = {x,y} implies x in X; :: :: Difference of an unordered pair (or a singleton) and a set. :: theorem :: ZFMISC_1:64 z in X \ {x} iff z in X & z <> x; theorem :: ZFMISC_1:65 X \ {x} = X iff not x in X; theorem :: ZFMISC_1:66 X \ {x} = {} implies X = {} or X = {x}; theorem :: ZFMISC_1:67 {x} \ X = {x} iff not x in X; theorem :: ZFMISC_1:68 {x} \ X = {} iff x in X; theorem :: ZFMISC_1:69 {x} \ X = {} or {x} \ X = {x}; theorem :: ZFMISC_1:70 {x,y} \ X = {x} iff not x in X & (y in X or x = y); canceled; theorem :: ZFMISC_1:72 {x,y} \ X = {x,y} iff not x in X & not y in X; theorem :: ZFMISC_1:73 {x,y} \ X = {} iff x in X & y in X; theorem :: ZFMISC_1:74 {x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x,y}; theorem :: ZFMISC_1:75 X \ {x,y} = {} iff X = {} or X = {x} or X = {y} or X = {x,y}; :: :: Power Set. :: canceled 3; theorem :: ZFMISC_1:79 A c= B implies bool A c= bool B; theorem :: ZFMISC_1:80 { A } c= bool A; theorem :: ZFMISC_1:81 bool A \/ bool B c= bool (A \/ B); theorem :: ZFMISC_1:82 bool A \/ bool B = bool (A \/ B) implies A,B are_c=-comparable; theorem :: ZFMISC_1:83 bool (A /\ B) = bool A /\ bool B; theorem :: ZFMISC_1:84 bool (A \ B) c= { {} } \/ (bool A \ bool B); canceled; theorem :: ZFMISC_1:86 bool (A \ B) \/ bool (B \ A) c= bool (A \+\ B); :: :: Union of a set. :: canceled 5; theorem :: ZFMISC_1:92 X in A implies X c= union A; theorem :: ZFMISC_1:93 union { X,Y } = X \/ Y; theorem :: ZFMISC_1:94 (for X st X in A holds X c= Z) implies union A c= Z; theorem :: ZFMISC_1:95 A c= B implies union A c= union B; theorem :: ZFMISC_1:96 union (A \/ B) = union A \/ union B; theorem :: ZFMISC_1:97 union (A /\ B) c= union A /\ union B; theorem :: ZFMISC_1:98 (for X st X in A holds X misses B) implies union A misses B; theorem :: ZFMISC_1:99 union bool A = A; theorem :: ZFMISC_1:100 A c= bool union A; theorem :: ZFMISC_1:101 (for X,Y st X<>Y & X in A \/ B & Y in A \/ B holds X misses Y) implies union(A /\ B) = union A /\ union B; :: :: Cartesian product. :: theorem :: ZFMISC_1:102 z in [:X,Y:] implies ex x,y st [x,y] = z; theorem :: ZFMISC_1:103 A c= [:X,Y:] & z in A implies ex x,y st x in X & y in Y & z = [x,y]; theorem :: ZFMISC_1:104 z in [:X1, Y1:] /\ [:X2, Y2:] implies ex x,y st z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2; theorem :: ZFMISC_1:105 [:X,Y:] c= bool bool (X \/ Y); theorem :: ZFMISC_1:106 [x,y] in [:X,Y:] iff x in X & y in Y; theorem :: ZFMISC_1:107 [x,y] in [:X,Y:] implies [y,x] in [:Y,X:]; theorem :: ZFMISC_1:108 (for x,y holds [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:]) implies [:X1,Y1:]=[:X2,Y2:]; theorem :: ZFMISC_1:109 A c= [:X,Y:] & (for x,y st [x,y] in A holds [x,y] in B) implies A c= B; theorem :: ZFMISC_1:110 A c= [:X1,Y1:] & B c= [:X2,Y2:] & (for x,y holds [x,y] in A iff [x,y] in B) implies A = B; theorem :: ZFMISC_1:111 (for z st z in A ex x,y st z=[x,y]) & (for x,y st [x,y] in A holds [x,y] in B) implies A c= B; theorem :: ZFMISC_1:112 (for z st z in A ex x,y st z = [x,y]) & (for z st z in B ex x,y st z=[x,y]) & (for x,y holds [x,y] in A iff [x,y] in B) implies A = B; theorem :: ZFMISC_1:113 [:X,Y:] = {} iff X = {} or Y = {}; theorem :: ZFMISC_1:114 X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] implies X = Y; theorem :: ZFMISC_1:115 [:X,X:] = [:Y,Y:] implies X = Y; theorem :: ZFMISC_1:116 X c= [:X,X:] implies X = {}; theorem :: ZFMISC_1:117 Z <> {} & ([:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:]) implies X c= Y; theorem :: ZFMISC_1:118 X c= Y implies [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:]; theorem :: ZFMISC_1:119 X1 c= Y1 & X2 c= Y2 implies [:X1,X2:] c= [:Y1,Y2:]; theorem :: ZFMISC_1:120 [:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:] & [:Z, X \/ Y:] = [:Z, X:] \/ [:Z, Y:]; theorem :: ZFMISC_1:121 [:X1 \/ X2, Y1 \/ Y2:] = [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1:] \/ [:X2,Y2:]; theorem :: ZFMISC_1:122 [:X /\ Y, Z:] = [:X, Z:] /\ [:Y, Z:] & [:Z, X /\ Y:] = [:Z, X:] /\ [:Z, Y:]; theorem :: ZFMISC_1:123 [:X1 /\ X2, Y1 /\ Y2:] = [:X1,Y1:] /\ [:X2, Y2:]; theorem :: ZFMISC_1:124 A c= X & B c= Y implies [:A,Y:] /\ [:X,B:] = [:A,B:]; theorem :: ZFMISC_1:125 [:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:] & [:Z, X \ Y:] = [:Z, X:] \ [:Z, Y:]; theorem :: ZFMISC_1:126 [:X1,X2:] \ [:Y1,Y2:] = [:X1\Y1,X2:] \/ [:X1,X2\Y2:]; theorem :: ZFMISC_1:127 X1 misses X2 or Y1 misses Y2 implies [:X1,Y1:] misses [:X2,Y2:]; theorem :: ZFMISC_1:128 [x,y] in [:{z},Y:] iff x = z & y in Y; theorem :: ZFMISC_1:129 [x,y] in [:X,{z}:] iff x in X & y = z; theorem :: ZFMISC_1:130 X <> {} implies [:{x},X:] <> {} & [:X,{x}:] <> {}; theorem :: ZFMISC_1:131 x <> y implies [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:]; theorem :: ZFMISC_1:132 [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:]; canceled; theorem :: ZFMISC_1:134 X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] implies X1 = X2 & Y1 = Y2; theorem :: ZFMISC_1:135 X c= [:X,Y:] or X c= [:Y,X:] implies X = {}; theorem :: ZFMISC_1:136 ex M st N in M & (for X,Y holds X in M & Y c= X implies Y in M) & (for X holds X in M implies bool X in M) & (for X holds X c= M implies X,M are_equipotent or X in M);

Back to top