:: Some Basic Properties of Sets :: by Czes{\l}aw Byli\'nski :: :: Received February 1, 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, TARSKI, ZFMISC_1; notations TARSKI, XBOOLE_0, ENUMSET1; constructors TARSKI, XBOOLE_0, ENUMSET1; registrations XBOOLE_0; requirements BOOLE; begin reserve u,v,x,x1,x2,y,y1,y2,z,p,a for object, A,B,X,X1,X2,X3,X4,Y,Y1,Y2,Z,N,M for set; definition let X; func bool X -> set means :: ZFMISC_1:def 1 Z in it iff Z c= X; end; definition let X1,X2; func [: X1,X2 :] -> set 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 :] -> set equals :: ZFMISC_1:def 3 [:[:X1,X2:],X3:]; end; definition let X1,X2,X3,X4; func [: X1,X2,X3,X4 :] -> set 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. :: theorem :: ZFMISC_1:3 {x} c= {y} implies x = y; theorem :: ZFMISC_1:4 {x} = {y1,y2} implies x = y1; theorem :: ZFMISC_1:5 {x} = {y1,y2} implies y1 = y2; theorem :: ZFMISC_1:6 { x1,x2 } = { y1,y2 } implies x1 = y1 or x1 = y2; theorem :: ZFMISC_1:7 {x} c= {x,y}; theorem :: ZFMISC_1:8 {x} \/ {y} = {x} implies x = y; theorem :: ZFMISC_1:9 {x} \/ {x,y} = {x,y}; theorem :: ZFMISC_1:10 {x} misses {y} implies x <> y; theorem :: ZFMISC_1:11 x <> y implies {x} misses {y}; theorem :: ZFMISC_1:12 {x} /\ {y} = {x} implies x = y; theorem :: ZFMISC_1:13 {x} /\ {x,y} = {x}; theorem :: ZFMISC_1:14 {x} \ {y} = {x} iff x <> y; theorem :: ZFMISC_1:15 {x} \ {y} = {} implies x = y; theorem :: ZFMISC_1:16 {x} \ {x,y} = {}; theorem :: ZFMISC_1:17 x <> y implies { x,y } \ { y } = { x }; theorem :: ZFMISC_1:18 {x} c= {y} implies x = y; theorem :: ZFMISC_1:19 {z} c= {x,y} implies z = x or z = y; theorem :: ZFMISC_1:20 {x,y} c= {z} implies x = z; theorem :: ZFMISC_1:21 {x,y} c= {z} implies {x,y} = {z}; theorem :: ZFMISC_1:22 {x1,x2} c= {y1,y2} implies x1 = y1 or x1 = y2; theorem :: ZFMISC_1:23 x <> y implies { x } \+\ { y } = { x,y }; theorem :: ZFMISC_1:24 bool { x } = { {} , { x }}; registration let x be object; reduce union { x } to x; end; theorem :: ZFMISC_1:25 union { x } = x; theorem :: ZFMISC_1:26 union {{x},{y}} = {x,y}; ::\$CT theorem :: ZFMISC_1:28 [x,y] in [:{x1},{y1}:] iff x = x1 & y = y1; theorem :: ZFMISC_1:29 [:{x},{y}:] = {[x,y]}; theorem :: ZFMISC_1:30 [:{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:31 {x} c= X iff x in X; theorem :: ZFMISC_1:32 {x1,x2} c= Z iff x1 in Z & x2 in Z; :: :: Set included in a singleton (or unordered pair). :: theorem :: ZFMISC_1:33 Y c= { x } iff Y = {} or Y = { x }; theorem :: ZFMISC_1:34 Y c= X & not x in Y implies Y c= X \ { x }; theorem :: ZFMISC_1:35 X <> {x} & X <> {} implies ex y st y in X & y <> x; theorem :: ZFMISC_1:36 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:37 {z} = X \/ Y implies X = {z} & Y = {z} or X = {} & Y = {z} or X = {z} & Y = {}; theorem :: ZFMISC_1:38 {z} = X \/ Y & X <> Y implies X = {} or Y = {}; theorem :: ZFMISC_1:39 {x} \/ X c= X implies x in X; theorem :: ZFMISC_1:40 x in X implies {x} \/ X = X; theorem :: ZFMISC_1:41 {x,y} \/ Z c= Z implies x in Z; theorem :: ZFMISC_1:42 x in Z & y in Z implies {x,y} \/ Z = Z; theorem :: ZFMISC_1:43 {x} \/ X <> {}; theorem :: ZFMISC_1:44 {x,y} \/ X <> {}; :: :: Intersection of an unordered pair (or a singleton) and a set. :: theorem :: ZFMISC_1:45 X /\ {x} = {x} implies x in X; theorem :: ZFMISC_1:46 x in X implies X /\ {x} = {x}; theorem :: ZFMISC_1:47 x in Z & y in Z implies {x,y} /\ Z = {x,y}; theorem :: ZFMISC_1:48 {x} misses X implies not x in X; theorem :: ZFMISC_1:49 {x,y} misses Z implies not x in Z; theorem :: ZFMISC_1:50 not x in X implies {x} misses X; theorem :: ZFMISC_1:51 not x in Z & not y in Z implies {x,y} misses Z; theorem :: ZFMISC_1:52 {x} misses X or {x} /\ X = {x}; theorem :: ZFMISC_1:53 {x,y} /\ X = {x} implies not y in X or x = y; theorem :: ZFMISC_1:54 x in X & (not y in X or x = y) implies {x,y} /\ X = {x}; theorem :: ZFMISC_1:55 {x,y} /\ X = {x,y} implies x in X; :: :: Difference of an unordered pair (or a singleton) and a set. :: theorem :: ZFMISC_1:56 z in X \ {x} iff z in X & z <> x; theorem :: ZFMISC_1:57 X \ {x} = X iff not x in X; theorem :: ZFMISC_1:58 X \ {x} = {} implies X = {} or X = {x}; theorem :: ZFMISC_1:59 {x} \ X = {x} iff not x in X; theorem :: ZFMISC_1:60 {x} \ X = {} iff x in X; theorem :: ZFMISC_1:61 {x} \ X = {} or {x} \ X = {x}; theorem :: ZFMISC_1:62 {x,y} \ X = {x} iff not x in X & (y in X or x = y); theorem :: ZFMISC_1:63 {x,y} \ X = {x,y} iff not x in X & not y in X; theorem :: ZFMISC_1:64 {x,y} \ X = {} iff x in X & y in X; theorem :: ZFMISC_1:65 {x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x ,y}; theorem :: ZFMISC_1:66 X \ {x,y} = {} iff X = {} or X = {x} or X = {y} or X = {x,y}; :: :: Power Set. :: theorem :: ZFMISC_1:67 A c= B implies bool A c= bool B; theorem :: ZFMISC_1:68 { A } c= bool A; theorem :: ZFMISC_1:69 bool A \/ bool B c= bool (A \/ B); theorem :: ZFMISC_1:70 bool A \/ bool B = bool (A \/ B) implies A,B are_c=-comparable; theorem :: ZFMISC_1:71 bool (A /\ B) = bool A /\ bool B; theorem :: ZFMISC_1:72 bool (A \ B) c= { {} } \/ (bool A \ bool B); theorem :: ZFMISC_1:73 bool (A \ B) \/ bool (B \ A) c= bool (A \+\ B); :: :: Union of a set. :: theorem :: ZFMISC_1:74 X in A implies X c= union A; theorem :: ZFMISC_1:75 union { X,Y } = X \/ Y; theorem :: ZFMISC_1:76 (for X st X in A holds X c= Z) implies union A c= Z; theorem :: ZFMISC_1:77 A c= B implies union A c= union B; theorem :: ZFMISC_1:78 union (A \/ B) = union A \/ union B; theorem :: ZFMISC_1:79 union (A /\ B) c= union A /\ union B; theorem :: ZFMISC_1:80 (for X st X in A holds X misses B) implies union A misses B; theorem :: ZFMISC_1:81 union bool A = A; theorem :: ZFMISC_1:82 A c= bool union A; theorem :: ZFMISC_1:83 (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:84 A c= [:X,Y:] & z in A implies ex x,y st x in X & y in Y & z = [ x,y]; theorem :: ZFMISC_1:85 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:86 [:X,Y:] c= bool bool (X \/ Y); theorem :: ZFMISC_1:87 for x,y being object holds [x,y] in [:X,Y:] iff x in X & y in Y; theorem :: ZFMISC_1:88 [x,y] in [:X,Y:] implies [y,x] in [:Y,X:]; theorem :: ZFMISC_1:89 (for x,y holds [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:]) implies [:X1 ,Y1:]=[:X2,Y2:]; theorem :: ZFMISC_1:90 [:X,Y:] = {} iff X = {} or Y = {}; theorem :: ZFMISC_1:91 X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] implies X = Y; theorem :: ZFMISC_1:92 [:X,X:] = [:Y,Y:] implies X = Y; theorem :: ZFMISC_1:93 X c= [:X,Y:] implies X = {}; theorem :: ZFMISC_1:94 Z <> {} & ([:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:]) implies X c= Y; theorem :: ZFMISC_1:95 X c= Y implies [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:]; theorem :: ZFMISC_1:96 X1 c= Y1 & X2 c= Y2 implies [:X1,X2:] c= [:Y1,Y2:]; theorem :: ZFMISC_1:97 [:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:] & [:Z, X \/ Y:] = [:Z, X:] \/ [:Z, Y:]; theorem :: ZFMISC_1:98 [:X1 \/ X2, Y1 \/ Y2:] = [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1:] \/ [:X2, Y2:]; theorem :: ZFMISC_1:99 [:X /\ Y, Z:] = [:X, Z:] /\ [:Y, Z:] & [:Z, X /\ Y:] = [:Z, X:] /\ [:Z , Y :] ; theorem :: ZFMISC_1:100 [:X1 /\ X2, Y1 /\ Y2:] = [:X1,Y1:] /\ [:X2, Y2:]; theorem :: ZFMISC_1:101 A c= X & B c= Y implies [:A,Y:] /\ [:X,B:] = [:A,B:]; theorem :: ZFMISC_1:102 [:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:] & [:Z, X \ Y:] = [:Z, X:] \ [:Z, Y:]; theorem :: ZFMISC_1:103 [:X1,X2:] \ [:Y1,Y2:] = [:X1\Y1,X2:] \/ [:X1,X2\Y2:]; theorem :: ZFMISC_1:104 X1 misses X2 or Y1 misses Y2 implies [:X1,Y1:] misses [:X2,Y2:]; theorem :: ZFMISC_1:105 [x,y] in [:{z},Y:] iff x = z & y in Y; theorem :: ZFMISC_1:106 [x,y] in [:X,{z}:] iff x in X & y = z; theorem :: ZFMISC_1:107 X <> {} implies [:{x},X:] <> {} & [:X,{x}:] <> {}; theorem :: ZFMISC_1:108 x <> y implies [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:]; theorem :: ZFMISC_1:109 [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X, {y} :] ; theorem :: ZFMISC_1:110 X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] implies X1 = X2 & Y1 = Y2; theorem :: ZFMISC_1:111 X c= [:X,Y:] or X c= [:Y,X:] implies X = {}; theorem :: ZFMISC_1:112 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; reserve e for object, X,X1,X2,Y1,Y2 for set; theorem :: ZFMISC_1:113 e in [:X1,Y1:] & e in [:X2,Y2:] implies e in [:X1 /\ X2, Y1 /\ Y2:]; begin :: Addenda :: from BORSUK_1 theorem :: ZFMISC_1:114 [:X1,X2:] c= [:Y1,Y2:] & [:X1,X2:] <> {} implies X1 c= Y1 & X2 c= Y2; :: from ALTCAT_1 theorem :: ZFMISC_1:115 for A being non empty set, B,C,D being set st [:A,B:] c= [:C,D:] or [: B,A:] c= [:D,C:] holds B c= D; theorem :: ZFMISC_1:116 x in X implies (X\{x})\/{x}=X; theorem :: ZFMISC_1:117 not x in X implies (X\/{x})\{x}=X; :: from WAYBEL18, 2006.01.06, A.T. theorem :: ZFMISC_1:118 for x,y,z,Z being set holds Z c= {x,y,z} iff Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z}; :: from PARTFUN1, 2006.12.05, A.T. theorem :: ZFMISC_1:119 N c= [:X1,Y1:] & M c= [:X2,Y2:] implies N \/ M c= [:X1 \/ X2,Y1 \/ Y2 :]; theorem :: ZFMISC_1:120 not x in X & not y in X implies X = X \ {x,y}; theorem :: ZFMISC_1:121 not x in X & not y in X implies X = X \/ {x,y} \ {x,y}; :: from INCPROJ, 2007.01.18. AK definition let x1, x2, x3 be object; pred x1, x2, x3 are_mutually_distinct means :: ZFMISC_1:def 5 x1 <> x2 & x1 <> x3 & x2 <> x3; end; definition let x1, x2, x3, x4 be object; pred x1, x2, x3, x4 are_mutually_distinct means :: ZFMISC_1:def 6 x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4; end; :: from CARD_2, 2007.01.18. AK definition let x1, x2, x3, x4, x5 be object; pred x1, x2, x3, x4, x5 are_mutually_distinct means :: ZFMISC_1:def 7 x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5; end; :: from BORSUK_5, 2007.01.18. AK definition let x1, x2, x3, x4, x5, x6 be object; pred x1, x2, x3, x4, x5, x6 are_mutually_distinct means :: ZFMISC_1:def 8 x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x4 <> x5 & x4 <> x6 & x5 <> x6; end; definition let x1, x2, x3, x4, x5, x6, x7 be object; pred x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct means :: ZFMISC_1:def 9 x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 & x4 <> x5 & x4 <> x6 & x4 <> x7 & x5 <> x6 & x5 <> x7 & x6 <> x7; end; :: missing, 2007.02.11, A.T. theorem :: ZFMISC_1:122 [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}; :: missing, 2008.03.22, A.T. theorem :: ZFMISC_1:123 x <> y implies A \/ {x} \ {y} = A \ {y} \/ {x}; :: comp. REALSET1, 2008.07.05, A.T. definition let X; attr X is trivial means :: ZFMISC_1:def 10 x in X & y in X implies x = y; end; registration cluster empty -> trivial for set; end; registration cluster non trivial -> non empty for set; end; registration let x; cluster {x} -> trivial; end; registration cluster trivial non empty for set; end; :: from SPRECT_3, 2008.09.30, A.T. theorem :: ZFMISC_1:124 for A,B,C being set, p be object st A c= B & B /\ C = {p} & p in A holds A /\ C = {p}; :: from SPRECT_2, 2008.09.30, A.T. theorem :: ZFMISC_1:125 for A,B,C being set st A /\ B c= {p} & p in C & C misses B holds A \/ C misses B; theorem :: ZFMISC_1:126 for A,B being set st for x,y being set st x in A & y in B holds x misses y holds union A misses union B; :: from BORSUK_3, 2009.01.24, A.T. registration let X be set, Y be empty set; cluster [:X, Y:] -> empty; end; registration let X be empty set, Y be set; cluster [:X, Y:] -> empty; end; :: new, 2009.08.26, A.T theorem :: ZFMISC_1:127 not A in [:A,B:]; theorem :: ZFMISC_1:128 B = [x,{x}] implies B in [:{x},B:]; theorem :: ZFMISC_1:129 B in [:A,B:] implies ex x being object st x in A & B = [x,{x}]; theorem :: ZFMISC_1:130 B c= A & A is trivial implies B is trivial; registration cluster non trivial for set; end; theorem :: ZFMISC_1:131 X is non empty trivial implies ex x st X = {x}; theorem :: ZFMISC_1:132 for x being set, X being trivial set st x in X holds X = {x}; :: from JORDAN16, 2011.04.27, A.T. theorem :: ZFMISC_1:133 for a,b,c,X being set st a in X & b in X & c in X holds {a,b,c} c= X; :: Lemma from RELAT_1, FUNCT_4 theorem :: ZFMISC_1:134 [x,y] in X implies x in union union X & y in union union X; theorem :: ZFMISC_1:135 X c= Y \/ {x} implies x in X or X c= Y; theorem :: ZFMISC_1:136 x in X \/ {y} iff x in X or x = y; theorem :: ZFMISC_1:137 X \/ {x} c= Y iff x in Y & X c= Y; theorem :: ZFMISC_1:138 for A, B being set st A c= B & B c= A \/ {a} holds A \/ {a} = B or A = B; registration let A,B be trivial set; cluster [:A,B:] -> trivial; end; :: from REALSET1, 2012.08.12, A.T. theorem :: ZFMISC_1:139 for X being set holds X is non trivial iff for x holds X\{x} is non empty;