:: Some Basic Properties of Sets
:: by Czes{\l}aw Byli\'nski
::
:: Received February 1, 1989
:: Copyright (c) 1990-2016 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,X:] 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;