:: Some Basic Properties of Sets
:: by Czes{\l}aw Byli\'nski
::
:: Received February 1, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

registration

let x, y be set ;
cluster [x,y] -> non empty ;
coherence
not [x,y] is empty ;

end;

Lm1: for x, X being set holds
( {x} c= X iff x in X )

proof end;

Lm2: for Y, X, x being set st Y c= X & not x in Y holds
Y c= X \ {x}

proof end;

Lm3: for Y, x being set holds
( Y c= {x} iff ( Y = {} or Y = {x} ) )

proof end;

definition

let X be set ;
defpred S₁[ set ] means $1 c= X;
func bool X -> set means :Def1: :: ZFMISC_1:def 1
for Z being set holds
( Z in it iff Z c= X );
existence
ex b₁ being set st
for Z being set holds
( Z in b₁ iff Z c= X )

proof end;

uniqueness
for b₁, b₂ being set st ( for Z being set holds
( Z in b₁ iff Z c= X ) ) & ( for Z being set holds
( Z in b₂ iff Z c= X ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines bool ZFMISC_1:def 1 :
for X being set
for b₂ being set holds
( b₂ = bool X iff for Z being set holds
( Z in b₂ iff Z c= X ) );

definition

let X1, X2 be set ;
defpred S₁[ 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 b₁ being set st
for z being set holds
( z in b₁ iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for z being set holds
( z in b₁ iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) ) ) & ( for z being set holds
( z in b₂ iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines [: ZFMISC_1:def 2 :
for X1, X2 being set
for b₃ being set holds
( b₃ = [:X1,X2:] iff for z being set holds
( z in b₃ iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) ) );

definition

let X1, X2, X3 be set ;
func [:X1,X2,X3:] -> set equals :: ZFMISC_1:def 3
[:[:X1,X2:],X3:];
coherence
[:[:X1,X2:],X3:] is set ;

end;

:: deftheorem defines [: ZFMISC_1:def 3 :
for X1, X2, X3 being set holds [:X1,X2,X3:] = [:[:X1,X2:],X3:];

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 :
for X1, X2, X3, X4 being set holds [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:];

begin

theorem :: ZFMISC_1:1

bool {} = {{}}

proof end;

theorem :: ZFMISC_1:2

union {} = {}

proof end;

theorem :: ZFMISC_1:3

canceled;

theorem :: ZFMISC_1:4

canceled;

theorem :: ZFMISC_1:5

canceled;

theorem Th6: :: ZFMISC_1:6

for x, y being set st {x} c= {y} holds
x = y

proof end;

theorem :: ZFMISC_1:7

canceled;

theorem Th8: :: ZFMISC_1:8

for x, y1, y2 being set st {x} = {y1,y2} holds
x = y1

proof end;

theorem Th9: :: ZFMISC_1:9

for x, y1, y2 being set st {x} = {y1,y2} holds
y1 = y2

proof end;

theorem Th10: :: ZFMISC_1:10

for x1, x2, y1, y2 being set holds
( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 )

proof end;

theorem :: ZFMISC_1:11

canceled;

theorem Th12: :: ZFMISC_1:12

for x, y being set holds {x} c= {x,y}

proof end;

Lm4: for x, X being set st {x} \/ X c= X holds
x in X

proof end;

theorem :: ZFMISC_1:13

for x, y being set st {x} \/ {y} = {x} holds
x = y

proof end;

Lm5: for x, X being set st x in X holds
{x} \/ X = X

proof end;

theorem :: ZFMISC_1:14

for x, y being set holds {x} \/ {x,y} = {x,y}

proof end;

Lm6: for x, X being set st {x} misses X holds
not x in X

proof end;

theorem :: ZFMISC_1:15

canceled;

theorem :: ZFMISC_1:16

for x, y being set st {x} misses {y} holds
x <> y

proof end;

Lm7: for x, X being set st not x in X holds
{x} misses X

proof end;

theorem Th17: :: ZFMISC_1:17

for x, y being set st x <> y holds
{x} misses {y}

proof end;

Lm8: for X, x being set st X /\ {x} = {x} holds
x in X

proof end;

theorem :: ZFMISC_1:18

for x, y being set st {x} /\ {y} = {x} holds
x = y

proof end;

Lm9: for x, X being set st x in X holds
X /\ {x} = {x}

proof end;

theorem :: ZFMISC_1:19

for x, y being set holds {x} /\ {x,y} = {x}

proof end;

Lm10: for x, X being set holds
( {x} \ X = {x} iff not x in X )

proof end;

theorem :: ZFMISC_1:20

for x, y being set holds
( {x} \ {y} = {x} iff x <> y )

proof end;

Lm11: for x, X being set holds
( {x} \ X = {} iff x in X )

proof end;

theorem :: ZFMISC_1:21

for x, y being set st {x} \ {y} = {} holds
x = y

proof end;

theorem :: ZFMISC_1:22

for x, y being set holds {x} \ {x,y} = {}

proof end;

Lm12: for x, y, X being set holds
( {x,y} \ X = {x} iff ( not x in X & ( y in X or x = y ) ) )

proof end;

theorem :: ZFMISC_1:23

for x, y being set st x <> y holds
{x,y} \ {y} = {x}

proof end;

theorem :: ZFMISC_1:24

for x, y being set st {x} c= {y} holds
x = y by Th6;

theorem :: ZFMISC_1:25

for z, x, y being set holds
( not {z} c= {x,y} or z = x or z = y )

proof end;

theorem Th26: :: ZFMISC_1:26

for x, y, z being set st {x,y} c= {z} holds
x = z

proof end;

theorem :: ZFMISC_1:27

for x, y, z being set st {x,y} c= {z} holds
{x,y} = {z}

proof end;

Lm13: for X, x being set st X <> {x} & X <> {} holds
ex y being set st
( y in X & y <> x )

proof end;

Lm14: for Z, x1, x2 being set holds
( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) )

proof end;

theorem :: ZFMISC_1:28

for x1, x2, y1, y2 being set holds
( not {x1,x2} c= {y1,y2} or x1 = y1 or x1 = y2 )

proof end;

theorem :: ZFMISC_1:29

for x, y being set st x <> y holds
{x} \+\ {y} = {x,y}

proof end;

theorem :: ZFMISC_1:30

for x being set holds bool {x} = {{},{x}}

proof end;

Lm15: for X, A being set st X in A holds
X c= union A

proof end;

theorem :: ZFMISC_1:31

for x being set holds union {x} = x

proof end;

Lm16: for X, Y being set holds union {X,Y} = X \/ Y

proof end;

theorem :: ZFMISC_1:32

for x, y being set holds union {{x},{y}} = {x,y}

proof end;

theorem Th33: :: ZFMISC_1:33

for x1, x2, y1, y2 being set st [x1,x2] = [y1,y2] holds
( x1 = y1 & x2 = y2 )

proof end;

Lm17: for x, y, X, Y being set holds
( [x,y] in [:X,Y:] iff ( x in X & y in Y ) )

proof end;

theorem :: ZFMISC_1:34

for x, y, x1, y1 being set holds
( [x,y] in [:{x1},{y1}:] iff ( x = x1 & y = y1 ) )

proof end;

theorem :: ZFMISC_1:35

for x, y being set holds [:{x},{y}:] = {[x,y]}

proof end;

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]} )

proof end;

theorem :: ZFMISC_1:37

for x, X being set holds
( {x} c= X iff x in X ) by Lm1;

theorem Th38: :: ZFMISC_1:38

for x1, x2, Z being set holds
( {x1,x2} c= Z iff ( x1 in Z & x2 in Z ) )

proof end;

theorem :: ZFMISC_1:39

for Y, x being set holds
( Y c= {x} iff ( Y = {} or Y = {x} ) ) by Lm3;

theorem :: ZFMISC_1:40

for Y, X, x being set st Y c= X & not x in Y holds
Y c= X \ {x} by Lm2;

theorem :: ZFMISC_1:41

for X, x being set st X <> {x} & X <> {} holds
ex y being set st
( y in X & y <> x ) by Lm13;

theorem :: ZFMISC_1:42

for Z, x1, x2 being set holds
( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) ) by Lm14;

theorem Th43: :: ZFMISC_1:43

for z, X, Y being set holds
( not {z} = X \/ Y or ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) )

proof end;

theorem :: ZFMISC_1:44

for z, X, Y being set st {z} = X \/ Y & X <> Y & not X = {} holds
Y = {}

proof end;

theorem :: ZFMISC_1:45

for x, X being set st {x} \/ X c= X holds
x in X by Lm4;

theorem :: ZFMISC_1:46

for x, X being set st x in X holds
{x} \/ X = X by Lm5;

theorem :: ZFMISC_1:47

for x, y, Z being set st {x,y} \/ Z c= Z holds
x in Z

proof end;

theorem :: ZFMISC_1:48

for x, Z, y being set st x in Z & y in Z holds
{x,y} \/ Z = Z

proof end;

theorem :: ZFMISC_1:49

for x, X being set holds {x} \/ X <> {} ;

theorem :: ZFMISC_1:50

for x, y, X being set holds {x,y} \/ X <> {} ;

theorem :: ZFMISC_1:51

for X, x being set st X /\ {x} = {x} holds
x in X by Lm8;

theorem :: ZFMISC_1:52

for x, X being set st x in X holds
X /\ {x} = {x} by Lm9;

theorem :: ZFMISC_1:53

for x, Z, y being set st x in Z & y in Z holds
{x,y} /\ Z = {x,y}

proof end;

theorem :: ZFMISC_1:54

for x, X being set st {x} misses X holds
not x in X by Lm6;

theorem Th55: :: ZFMISC_1:55

for x, y, Z being set st {x,y} misses Z holds
not x in Z

proof end;

theorem :: ZFMISC_1:56

for x, X being set st not x in X holds
{x} misses X by Lm7;

theorem Th57: :: ZFMISC_1:57

for x, Z, y being set st not x in Z & not y in Z holds
{x,y} misses Z

proof end;

theorem :: ZFMISC_1:58

for x, X being set holds
( {x} misses X or {x} /\ X = {x} ) by Lm7, Lm9;

theorem :: ZFMISC_1:59

for x, y, X being set holds
( not {x,y} /\ X = {x} or not y in X or x = y )

proof end;

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}

proof end;

theorem :: ZFMISC_1:61

canceled;

theorem :: ZFMISC_1:62

canceled;

theorem :: ZFMISC_1:63

for x, y, X being set st {x,y} /\ X = {x,y} holds
x in X

proof end;

theorem Th64: :: ZFMISC_1:64

for z, X, x being set holds
( z in X \ {x} iff ( z in X & z <> x ) )

proof end;

theorem Th65: :: ZFMISC_1:65

for X, x being set holds
( X \ {x} = X iff not x in X )

proof end;

theorem :: ZFMISC_1:66

for X, x being set holds
( not X \ {x} = {} or X = {} or X = {x} )

proof end;

theorem :: ZFMISC_1:67

for x, X being set holds
( {x} \ X = {x} iff not x in X ) by Lm10;

theorem :: ZFMISC_1:68

for x, X being set holds
( {x} \ X = {} iff x in X ) by Lm11;

theorem :: ZFMISC_1:69

for x, X being set holds
( {x} \ X = {} or {x} \ X = {x} )

proof end;

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 ) )

proof end;

theorem Th73: :: ZFMISC_1:73

for x, y, X being set holds
( {x,y} \ X = {} iff ( x in X & y in X ) )

proof end;

theorem :: ZFMISC_1:74

for x, y, X being set holds
( {x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x,y} )

proof end;

theorem :: ZFMISC_1:75

for X, x, y being set holds
( X \ {x,y} = {} iff ( X = {} or X = {x} or X = {y} or X = {x,y} ) )

proof end;

theorem :: ZFMISC_1:76

canceled;

theorem :: ZFMISC_1:77

canceled;

theorem :: ZFMISC_1:78

canceled;

theorem :: ZFMISC_1:79

for A, B being set st A c= B holds
bool A c= bool B

proof end;

theorem :: ZFMISC_1:80

for A being set holds {A} c= bool A

proof end;

theorem :: ZFMISC_1:81

for A, B being set holds (bool A) \/ (bool B) c= bool (A \/ B)

proof end;

theorem :: ZFMISC_1:82

for A, B being set st (bool A) \/ (bool B) = bool (A \/ B) holds
A,B are_c=-comparable

proof end;

theorem :: ZFMISC_1:83

for A, B being set holds bool (A /\ B) = (bool A) /\ (bool B)

proof end;

theorem :: ZFMISC_1:84

for A, B being set holds bool (A \ B) c= {{}} \/ ((bool A) \ (bool B))

proof end;

theorem :: ZFMISC_1:85

canceled;

theorem :: ZFMISC_1:86

for A, B being set holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)

proof end;

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

for X, A being set st X in A holds
X c= union A by Lm15;

theorem :: ZFMISC_1:93

for X, Y being set holds union {X,Y} = X \/ Y by Lm16;

theorem :: ZFMISC_1:94

for A, Z being set st ( for X being set st X in A holds
X c= Z ) holds
union A c= Z

proof end;

theorem Th95: :: ZFMISC_1:95

for A, B being set st A c= B holds
union A c= union B

proof end;

theorem :: ZFMISC_1:96

for A, B being set holds union (A \/ B) = (union A) \/ (union B)

proof end;

theorem Th97: :: ZFMISC_1:97

for A, B being set holds union (A /\ B) c= (union A) /\ (union B)

proof end;

theorem Th98: :: ZFMISC_1:98

for A, B being set st ( for X being set st X in A holds
X misses B ) holds
union A misses B

proof end;

theorem :: ZFMISC_1:99

for A being set holds union (bool A) = A

proof end;

theorem :: ZFMISC_1:100

for A being set holds A c= bool (union A)

proof end;

theorem :: ZFMISC_1:101

for A, B being set st ( for X, Y being set st X <> Y & X in A \/ B & Y in A \/ B holds
X misses Y ) holds
union (A /\ B) = (union A) /\ (union B)

proof end;

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] )

proof end;

theorem Th104: :: ZFMISC_1:104

for z, X1, Y1, X2, Y2 being set st z in [:X1,Y1:] /\ [:X2,Y2:] holds
ex x, y being set st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 )

proof end;

theorem :: ZFMISC_1:105

for X, Y being set holds [:X,Y:] c= bool (bool (X \/ Y))

proof end;

theorem :: ZFMISC_1:106

for x, y, X, Y being set holds
( [x,y] in [:X,Y:] iff ( x in X & y in Y ) ) by Lm17;

theorem Th107: :: ZFMISC_1:107

for x, y, X, Y being set st [x,y] in [:X,Y:] holds
[y,x] in [:Y,X:]

proof end;

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:]

proof end;

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

proof end;

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

proof end;

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

for X, Y being set holds
( [:X,Y:] = {} iff ( X = {} or Y = {} ) )

proof end;

theorem :: ZFMISC_1:114

for X, Y being set st X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] holds
X = Y

proof end;

theorem :: ZFMISC_1:115

for X, Y being set st [:X,X:] = [:Y,Y:] holds
X = Y

proof end;

Lm20: for z, X, Y being set st z in [:X,Y:] holds
ex x, y being set st [x,y] = z

proof end;

theorem :: ZFMISC_1:116

for X being set st X c= [:X,X:] holds
X = {}

proof end;

theorem :: ZFMISC_1:117

for Z, X, Y being set st Z <> {} & ( [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:] ) holds
X c= Y

proof end;

theorem Th118: :: ZFMISC_1:118

for X, Y, Z being set st X c= Y holds
( [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:] )

proof end;

theorem Th119: :: ZFMISC_1:119

for X1, Y1, X2, Y2 being set st X1 c= Y1 & X2 c= Y2 holds
[:X1,X2:] c= [:Y1,Y2:]

proof end;

theorem Th120: :: ZFMISC_1:120

for X, Y, Z being set holds
( [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] & [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] )

proof end;

theorem :: ZFMISC_1:121

for X1, X2, Y1, Y2 being set holds [:(X1 \/ X2),(Y1 \/ Y2):] = (([:X1,Y1:] \/ [:X1,Y2:]) \/ [:X2,Y1:]) \/ [:X2,Y2:]

proof end;

theorem :: ZFMISC_1:122

for X, Y, Z being set holds
( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] & [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )

proof end;

theorem Th123: :: ZFMISC_1:123

for X1, X2, Y1, Y2 being set holds [:(X1 /\ X2),(Y1 /\ Y2):] = [:X1,Y1:] /\ [:X2,Y2:]

proof end;

theorem :: ZFMISC_1:124

for A, X, B, Y being set st A c= X & B c= Y holds
[:A,Y:] /\ [:X,B:] = [:A,B:]

proof end;

theorem Th125: :: ZFMISC_1:125

for X, Y, Z being set holds
( [:(X \ Y),Z:] = [:X,Z:] \ [:Y,Z:] & [:Z,(X \ Y):] = [:Z,X:] \ [:Z,Y:] )

proof end;

theorem :: ZFMISC_1:126

for X1, X2, Y1, Y2 being set holds [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]

proof end;

theorem Th127: :: ZFMISC_1:127

for X1, X2, Y1, Y2 being set st ( X1 misses X2 or Y1 misses Y2 ) holds
[:X1,Y1:] misses [:X2,Y2:]

proof end;

theorem :: ZFMISC_1:128

for x, y, z, Y being set holds
( [x,y] in [:{z},Y:] iff ( x = z & y in Y ) )

proof end;

theorem :: ZFMISC_1:129

for x, y, X, z being set holds
( [x,y] in [:X,{z}:] iff ( x in X & y = z ) )

proof end;

theorem :: ZFMISC_1:130

for X, x being set st X <> {} holds
( [:{x},X:] <> {} & [:X,{x}:] <> {} ) by Th113;

theorem :: ZFMISC_1:131

for x, y, X, Y being set st x <> y holds
( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )

proof end;

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}:] )

proof end;

theorem :: ZFMISC_1:133

canceled;

theorem Th134: :: ZFMISC_1:134

for X1, Y1, X2, Y2 being set st X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] holds
( X1 = X2 & Y1 = Y2 )

proof end;

theorem :: ZFMISC_1:135

for X, Y being set st ( X c= [:X,Y:] or X c= [:Y,X:] ) holds
X = {}

proof end;

theorem :: ZFMISC_1:136

for N being set ex M being set st
( N in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) & ( for X being set st X in M holds
bool X in M ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )

proof end;

theorem :: ZFMISC_1:137

for e, X1, Y1, X2, Y2 being set st e in [:X1,Y1:] & e in [:X2,Y2:] holds
e in [:(X1 /\ X2),(Y1 /\ Y2):]

proof end;

begin

theorem Th138: :: ZFMISC_1:138

for X1, X2, Y1, Y2 being set st [:X1,X2:] c= [:Y1,Y2:] & [:X1,X2:] <> {} holds
( X1 c= Y1 & X2 c= Y2 )

proof end;

theorem :: ZFMISC_1:139

for A being non empty set
for B, C, D being set st ( [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] ) holds
B c= D

proof end;

theorem :: ZFMISC_1:140

for x, X being set st x in X holds
(X \ {x}) \/ {x} = X

proof end;

theorem :: ZFMISC_1:141

for x, X being set st not x in X holds
(X \/ {x}) \ {x} = X

proof end;

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} ) )

proof end;

theorem :: ZFMISC_1:143

for N, M, X1, Y1, X2, Y2 being set st N c= [:X1,Y1:] & M c= [:X2,Y2:] holds
N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):]

proof end;

Lm21: for x, y, X being set st not x in X & not y in X holds
{x,y} misses X

proof end;

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}

proof end;

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}

proof end;

definition

let x1, x2, x3 be set ;
pred x1,x2,x3 are_mutually_different means :: ZFMISC_1:def 5
( x1 <> x2 & x1 <> x3 & x2 <> x3 );

end;

:: deftheorem defines are_mutually_different ZFMISC_1:def 5 :
for x1, x2, x3 being set holds
( x1,x2,x3 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x2 <> x3 ) );

definition

let x1, x2, x3, x4 be set ;
pred x1,x2,x3,x4 are_mutually_different means :: ZFMISC_1:def 6
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 );

end;

:: deftheorem defines are_mutually_different ZFMISC_1:def 6 :
for x1, x2, x3, x4 being set holds
( x1,x2,x3,x4 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 ) );

definition

let x1, x2, x3, x4, x5 be set ;
pred x1,x2,x3,x4,x5 are_mutually_different 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;

:: deftheorem defines are_mutually_different ZFMISC_1:def 7 :
for x1, x2, x3, x4, x5 being set holds
( x1,x2,x3,x4,x5 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5 ) );

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]}

proof end;

theorem :: ZFMISC_1:147

for x, y, A being set st x <> y holds
(A \/ {x}) \ {y} = (A \ {y}) \/ {x} by Th17, XBOOLE_1:87;

definition

let X be set ;
attr X is trivial means :: ZFMISC_1:def 10
for x, y being set st x in X & y in X holds
x = y;

end;

:: 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 );

registration

cluster empty -> trivial set ;
coherence
for b₁ being set st b₁ is empty holds
b₁ is trivial

proof end;

end;

registration

let x be set ;
cluster {x} -> trivial ;
coherence
{x} is trivial

proof end;

end;

theorem :: ZFMISC_1:148

for A, B, C, p being set st A c= B & B /\ C = {p} & p in A holds
A /\ C = {p}

proof end;

theorem :: ZFMISC_1:149

for A, B, C, p being set st A /\ B c= {p} & p in C & C misses B holds
A \/ C misses B

proof end;

theorem :: ZFMISC_1:150

canceled;

theorem :: ZFMISC_1:151

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

proof end;

registration

let X be set ;
let Y be empty set ;
cluster [:X,Y:] -> empty ;
coherence
[:X,Y:] is empty by Th113;

end;

registration

let X be empty set ;
let Y be set ;
cluster [:X,Y:] -> empty ;
coherence
[:X,Y:] is empty by Th113;

end;

theorem :: ZFMISC_1:152

for A, B being set holds not A in [:A,B:]

proof end;

theorem :: ZFMISC_1:153

for x being set holds [x,{x}] in [:{x},[x,{x}]:]

proof end;

theorem :: ZFMISC_1:154

for B, A being set st B in [:A,B:] holds
ex x being set st
( x in A & B = [x,{x}] )

proof end;