:: Some Basic Properties of Sets
:: by Czes{\l}aw Byli\'nski
::
:: Received February 1, 1989
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for x, X being set holds
( {x} c= X iff x in X )
Lm2:
for Y, X, x being set st Y c= X & not x in Y holds
Y c= X \ {x}
Lm3:
for Y, x being set holds
( Y c= {x} iff ( Y = {} or Y = {x} ) )
:: deftheorem Def1 defines bool ZFMISC_1:def 1 :
for
X being
set for
b2 being
set holds
(
b2 = bool X iff for
Z being
set holds
(
Z in b2 iff
Z c= X ) );
definition
let X1,
X2 be
set ;
defpred S1[
set ]
means ex
x,
y being
set st
(
x in X1 &
y in X2 & $1
= [x,y] );
func [:X1,X2:] -> set means :
Def2:
:: ZFMISC_1:def 2
for
z being
set holds
(
z in it iff ex
x,
y being
set st
(
x in X1 &
y in X2 &
z = [x,y] ) );
existence
ex b1 being set st
for z being set holds
( z in b1 iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) )
uniqueness
for b1, b2 being set st ( for z being set holds
( z in b1 iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) ) ) & ( for z being set holds
( z in b2 iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines [: ZFMISC_1:def 2 :
for
X1,
X2 being
set for
b3 being
set holds
(
b3 = [:X1,X2:] iff for
z being
set holds
(
z in b3 iff ex
x,
y being
set st
(
x in X1 &
y in X2 &
z = [x,y] ) ) );
:: deftheorem defines [: ZFMISC_1:def 3 :
definition
let X1,
X2,
X3,
X4 be
set ;
func [:X1,X2,X3,X4:] -> set equals :: ZFMISC_1:def 4
[:[:X1,X2,X3:],X4:];
coherence
[:[:X1,X2,X3:],X4:] is set
;
end;
:: deftheorem defines [: ZFMISC_1:def 4 :
theorem :: ZFMISC_1:1
theorem :: ZFMISC_1:2
theorem :: ZFMISC_1:3
canceled;
theorem :: ZFMISC_1:4
canceled;
theorem :: ZFMISC_1:5
canceled;
theorem Th6: :: ZFMISC_1:6
theorem :: ZFMISC_1:7
canceled;
theorem Th8: :: ZFMISC_1:8
for
x,
y1,
y2 being
set st
{x} = {y1,y2} holds
x = y1
theorem Th9: :: ZFMISC_1:9
for
x,
y1,
y2 being
set st
{x} = {y1,y2} holds
y1 = y2
theorem Th10: :: ZFMISC_1:10
for
x1,
x2,
y1,
y2 being
set holds
( not
{x1,x2} = {y1,y2} or
x1 = y1 or
x1 = y2 )
theorem :: ZFMISC_1:11
canceled;
theorem Th12: :: ZFMISC_1:12
Lm4:
for x, X being set st {x} \/ X c= X holds
x in X
theorem :: ZFMISC_1:13
Lm5:
for x, X being set st x in X holds
{x} \/ X = X
theorem :: ZFMISC_1:14
Lm6:
for x, X being set st {x} misses X holds
not x in X
theorem :: ZFMISC_1:15
canceled;
theorem :: ZFMISC_1:16
Lm7:
for x, X being set st not x in X holds
{x} misses X
theorem Th17: :: ZFMISC_1:17
Lm8:
for X, x being set st X /\ {x} = {x} holds
x in X
theorem :: ZFMISC_1:18
Lm9:
for x, X being set st x in X holds
X /\ {x} = {x}
theorem :: ZFMISC_1:19
Lm10:
for x, X being set holds
( {x} \ X = {x} iff not x in X )
theorem :: ZFMISC_1:20
Lm11:
for x, X being set holds
( {x} \ X = {} iff x in X )
theorem :: ZFMISC_1:21
theorem :: ZFMISC_1:22
Lm12:
for x, y, X being set holds
( {x,y} \ X = {x} iff ( not x in X & ( y in X or x = y ) ) )
theorem :: ZFMISC_1:23
theorem :: ZFMISC_1:24
theorem :: ZFMISC_1:25
for
z,
x,
y being
set holds
( not
{z} c= {x,y} or
z = x or
z = y )
theorem Th26: :: ZFMISC_1:26
theorem :: ZFMISC_1:27
Lm13:
for X, x being set st X <> {x} & X <> {} holds
ex y being set st
( y in X & y <> x )
Lm14:
for Z, x1, x2 being set holds
( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) )
theorem :: ZFMISC_1:28
for
x1,
x2,
y1,
y2 being
set holds
( not
{x1,x2} c= {y1,y2} or
x1 = y1 or
x1 = y2 )
theorem :: ZFMISC_1:29
theorem :: ZFMISC_1:30
Lm15:
for X, A being set st X in A holds
X c= union A
theorem :: ZFMISC_1:31
Lm16:
for X, Y being set holds union {X,Y} = X \/ Y
theorem :: ZFMISC_1:32
theorem Th33: :: ZFMISC_1:33
for
x1,
x2,
y1,
y2 being
set st
[x1,x2] = [y1,y2] holds
(
x1 = y1 &
x2 = y2 )
Lm17:
for x, y, X, Y being set holds
( [x,y] in [:X,Y:] iff ( x in X & y in Y ) )
theorem :: ZFMISC_1:34
theorem :: ZFMISC_1:35
theorem Th36: :: ZFMISC_1:36
for
x,
y,
z being
set holds
(
[:{x},{y,z}:] = {[x,y],[x,z]} &
[:{x,y},{z}:] = {[x,z],[y,z]} )
theorem :: ZFMISC_1:37
theorem Th38: :: ZFMISC_1:38
for
x1,
x2,
Z being
set holds
(
{x1,x2} c= Z iff (
x1 in Z &
x2 in Z ) )
theorem :: ZFMISC_1:39
theorem :: ZFMISC_1:40
theorem :: ZFMISC_1:41
theorem :: ZFMISC_1:42
theorem Th43: :: ZFMISC_1:43
theorem :: ZFMISC_1:44
theorem :: ZFMISC_1:45
theorem :: ZFMISC_1:46
theorem :: ZFMISC_1:47
theorem :: ZFMISC_1:48
for
x,
Z,
y being
set st
x in Z &
y in Z holds
{x,y} \/ Z = Z
theorem :: ZFMISC_1:49
theorem :: ZFMISC_1:50
theorem :: ZFMISC_1:51
theorem :: ZFMISC_1:52
theorem :: ZFMISC_1:53
theorem :: ZFMISC_1:54
theorem Th55: :: ZFMISC_1:55
theorem :: ZFMISC_1:56
theorem Th57: :: ZFMISC_1:57
theorem :: ZFMISC_1:58
theorem :: ZFMISC_1:59
for
x,
y,
X being
set holds
( not
{x,y} /\ X = {x} or not
y in X or
x = y )
theorem :: ZFMISC_1:60
for
x,
X,
y being
set st
x in X & ( not
y in X or
x = y ) holds
{x,y} /\ X = {x}
theorem :: ZFMISC_1:61
canceled;
theorem :: ZFMISC_1:62
canceled;
theorem :: ZFMISC_1:63
theorem Th64: :: ZFMISC_1:64
for
z,
X,
x being
set holds
(
z in X \ {x} iff (
z in X &
z <> x ) )
theorem Th65: :: ZFMISC_1:65
for
X,
x being
set holds
(
X \ {x} = X iff not
x in X )
theorem :: ZFMISC_1:66
theorem :: ZFMISC_1:67
theorem :: ZFMISC_1:68
theorem :: ZFMISC_1:69
theorem :: ZFMISC_1:70
for
x,
y,
X being
set holds
(
{x,y} \ X = {x} iff ( not
x in X & (
y in X or
x = y ) ) )
by Lm12;
theorem :: ZFMISC_1:71
canceled;
theorem Th72: :: ZFMISC_1:72
for
x,
y,
X being
set holds
(
{x,y} \ X = {x,y} iff ( not
x in X & not
y in X ) )
theorem Th73: :: ZFMISC_1:73
for
x,
y,
X being
set holds
(
{x,y} \ X = {} iff (
x in X &
y in X ) )
theorem :: ZFMISC_1:74
theorem :: ZFMISC_1:75
theorem :: ZFMISC_1:76
canceled;
theorem :: ZFMISC_1:77
canceled;
theorem :: ZFMISC_1:78
canceled;
theorem :: ZFMISC_1:79
theorem :: ZFMISC_1:80
theorem :: ZFMISC_1:81
theorem :: ZFMISC_1:82
theorem :: ZFMISC_1:83
theorem :: ZFMISC_1:84
theorem :: ZFMISC_1:85
canceled;
theorem :: ZFMISC_1:86
theorem :: ZFMISC_1:87
canceled;
theorem :: ZFMISC_1:88
canceled;
theorem :: ZFMISC_1:89
canceled;
theorem :: ZFMISC_1:90
canceled;
theorem :: ZFMISC_1:91
canceled;
theorem :: ZFMISC_1:92
theorem :: ZFMISC_1:93
theorem :: ZFMISC_1:94
theorem Th95: :: ZFMISC_1:95
theorem :: ZFMISC_1:96
theorem Th97: :: ZFMISC_1:97
theorem Th98: :: ZFMISC_1:98
theorem :: ZFMISC_1:99
theorem :: ZFMISC_1:100
theorem :: ZFMISC_1:101
theorem :: ZFMISC_1:102
canceled;
theorem Th103: :: ZFMISC_1:103
for
A,
X,
Y,
z being
set st
A c= [:X,Y:] &
z in A holds
ex
x,
y being
set st
(
x in X &
y in Y &
z = [x,y] )
theorem Th104: :: ZFMISC_1:104
theorem :: ZFMISC_1:105
theorem :: ZFMISC_1:106
theorem Th107: :: ZFMISC_1:107
theorem :: ZFMISC_1:108
for
X1,
Y1,
X2,
Y2 being
set st ( for
x,
y being
set holds
(
[x,y] in [:X1,Y1:] iff
[x,y] in [:X2,Y2:] ) ) holds
[:X1,Y1:] = [:X2,Y2:]
Lm18:
for A, X1, Y1, B, X2, Y2 being set st A c= [:X1,Y1:] & B c= [:X2,Y2:] & ( for x, y being set holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B
Lm19:
for A, B being set st ( for z being set st z in A holds
ex x, y being set st z = [x,y] ) & ( for z being set st z in B holds
ex x, y being set st z = [x,y] ) & ( for x, y being set holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B
theorem :: ZFMISC_1:109
canceled;
theorem :: ZFMISC_1:110
canceled;
theorem :: ZFMISC_1:111
canceled;
theorem :: ZFMISC_1:112
canceled;
theorem Th113: :: ZFMISC_1:113
theorem :: ZFMISC_1:114
theorem :: ZFMISC_1:115
Lm20:
for z, X, Y being set st z in [:X,Y:] holds
ex x, y being set st [x,y] = z
theorem :: ZFMISC_1:116
theorem :: ZFMISC_1:117
theorem Th118: :: ZFMISC_1:118
theorem Th119: :: ZFMISC_1:119
theorem Th120: :: ZFMISC_1:120
theorem :: ZFMISC_1:121
theorem :: ZFMISC_1:122
theorem Th123: :: ZFMISC_1:123
theorem :: ZFMISC_1:124
theorem Th125: :: ZFMISC_1:125
theorem :: ZFMISC_1:126
theorem Th127: :: ZFMISC_1:127
theorem Th128: :: ZFMISC_1:128
theorem Th129: :: ZFMISC_1:129
theorem :: ZFMISC_1:130
theorem :: ZFMISC_1:131
theorem :: ZFMISC_1:132
for
x,
y,
X being
set holds
(
[:{x,y},X:] = [:{x},X:] \/ [:{y},X:] &
[:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )
theorem :: ZFMISC_1:133
canceled;
theorem Th134: :: ZFMISC_1:134
theorem :: ZFMISC_1:135
theorem :: ZFMISC_1:136
theorem :: ZFMISC_1:137
theorem Th138: :: ZFMISC_1:138
theorem :: ZFMISC_1:139
theorem :: ZFMISC_1:140
theorem :: ZFMISC_1:141
theorem :: ZFMISC_1:142
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} ) )
theorem :: ZFMISC_1:143
Lm21:
for x, y, X being set st not x in X & not y in X holds
{x,y} misses X
theorem Th144: :: ZFMISC_1:144
for
x,
y,
X being
set st not
x in X & not
y in X holds
X = X \ {x,y}
theorem :: ZFMISC_1:145
for
x,
y,
X being
set st not
x in X & not
y in X holds
X = (X \/ {x,y}) \ {x,y}
:: deftheorem defines are_mutually_different ZFMISC_1:def 5 :
:: deftheorem defines are_mutually_different ZFMISC_1:def 6 :
:: deftheorem defines are_mutually_different ZFMISC_1:def 7 :
definition
let x1,
x2,
x3,
x4,
x5,
x6 be
set ;
pred x1,
x2,
x3,
x4,
x5,
x6 are_mutually_different 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;
:: deftheorem defines are_mutually_different ZFMISC_1:def 8 :
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
(
x1,
x2,
x3,
x4,
x5,
x6 are_mutually_different iff (
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 ) );
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7 be
set ;
pred x1,
x2,
x3,
x4,
x5,
x6,
x7 are_mutually_different 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;
:: deftheorem defines are_mutually_different ZFMISC_1:def 9 :
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
(
x1,
x2,
x3,
x4,
x5,
x6,
x7 are_mutually_different iff (
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 ) );
theorem :: ZFMISC_1:146
for
x1,
x2,
y1,
y2 being
set holds
[:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
theorem :: ZFMISC_1:147
:: deftheorem defines trivial ZFMISC_1:def 10 :
for
X being
set holds
(
X is
trivial iff for
x,
y being
set st
x in X &
y in X holds
x = y );
theorem :: ZFMISC_1:148
theorem :: ZFMISC_1:149
theorem :: ZFMISC_1:150
theorem :: ZFMISC_1:151
theorem :: ZFMISC_1:152
theorem :: ZFMISC_1:153
theorem :: ZFMISC_1:154