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

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

proof end;

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

proof end;

Lm3: for x being object
for Y 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, 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₁[ object ] means ex x, y being object st
( x in X1 & y in X2 & $1 = [x,y] );

func [:X1,X2:] -> set means :Def2: :: ZFMISC_1:def 2
for z being object holds
( z in it iff ex x, y being object st
( x in X1 & y in X2 & z = [x,y] ) );

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

proof end;

uniqueness
for b₁, b₂ being set st ( for z being object holds
( z in b₁ iff ex x, y being object st
( x in X1 & y in X2 & z = [x,y] ) ) ) & ( for z being object holds
( z in b₂ iff ex x, y being object 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, b₃ being set holds
( b₃ = [:X1,X2:] iff for z being object holds
( z in b₃ iff ex x, y being object 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:];

::
:: Empty set.
::

theorem :: ZFMISC_1:1

bool {} = {{}}

proof end;

theorem :: ZFMISC_1:2

union {} = {}

proof end;

::
:: Singleton and unordered pairs.
::

theorem Th3: :: ZFMISC_1:3

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

proof end;

theorem Th4: :: ZFMISC_1:4

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

proof end;

theorem :: ZFMISC_1:5

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

proof end;

theorem Th6: :: ZFMISC_1:6

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

proof end;

theorem Th7: :: ZFMISC_1:7

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

proof end;

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

proof end;

theorem :: ZFMISC_1:8

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

proof end;

theorem :: ZFMISC_1:9

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

proof end;

Lm5: for x being object
for X being set st {x} misses X holds
not x in X

proof end;

theorem :: ZFMISC_1:10

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

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

proof end;

theorem Th11: :: ZFMISC_1:11

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

proof end;

Lm7: for x being object
for X being set st X /\ {x} = {x} holds
x in X

proof end;

theorem :: ZFMISC_1:12

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

proof end;

Lm8: for x being object
for X being set st x in X holds
X /\ {x} = {x}
by Lm1, XBOOLE_1:28;

theorem :: ZFMISC_1:13

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

proof end;

Lm9: for x being object
for X being set holds
( {x} \ X = {x} iff not x in X )
by Lm5, Lm6, XBOOLE_1:83;

theorem :: ZFMISC_1:14

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

proof end;

Lm10: for x being object
for X being set holds
( {x} \ X = {} iff x in X )
by Lm1, XBOOLE_1:37;

theorem :: ZFMISC_1:15

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

proof end;

theorem :: ZFMISC_1:16

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

proof end;

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

proof end;

theorem :: ZFMISC_1:17

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

proof end;

theorem :: ZFMISC_1:18

for x, y being object st {x} c= {y} holds
x = y by Th3;

theorem :: ZFMISC_1:19

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

proof end;

theorem Th20: :: ZFMISC_1:20

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

proof end;

theorem :: ZFMISC_1:21

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

proof end;

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

proof end;

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

proof end;

theorem :: ZFMISC_1:22

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

proof end;

theorem :: ZFMISC_1:23

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

proof end;

theorem :: ZFMISC_1:24

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

proof end;

Lm14: for A, X being set st X in A holds
X c= union A
by TARSKI:def 4;

registration

let x be object ;

reduce union {x} to x;

reducibility
union {x} = x

proof end;

end;

theorem :: ZFMISC_1:25

for x being object holds union {x} = x ;

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

proof end;

theorem :: ZFMISC_1:26

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

proof end;

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

proof end;

theorem :: ZFMISC_1:27

canceled;

::$CT

theorem :: ZFMISC_1:28

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

proof end;

theorem Th28: :: ZFMISC_1:29

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

proof end;

theorem Th29: :: ZFMISC_1:30

for x, y, z being object holds
( [:{x},{y,z}:] = {[x,y],[x,z]} & [:{x,y},{z}:] = {[x,z],[y,z]} )

proof end;

::
:: Singleton and unordered pairs included in a set.
::

theorem :: ZFMISC_1:31

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

theorem Th31: :: ZFMISC_1:32

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

proof end;

::
:: Set included in a singleton (or unordered pair).
::

theorem :: ZFMISC_1:33

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

theorem :: ZFMISC_1:34

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

theorem :: ZFMISC_1:35

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

theorem :: ZFMISC_1:36

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

::
:: Sum of an unordered pair (or a singleton) and a set.
::

theorem Th36: :: ZFMISC_1:37

for z being object
for 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:38

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

proof end;

theorem :: ZFMISC_1:39

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

theorem :: ZFMISC_1:40

for x being object
for X being set st x in X holds
{x} \/ X = X by Lm1, XBOOLE_1:12;

theorem :: ZFMISC_1:41

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

proof end;

theorem :: ZFMISC_1:42

for x, y being object
for Z being set st x in Z & y in Z holds
{x,y} \/ Z = Z by Th31, XBOOLE_1:12;

theorem :: ZFMISC_1:43

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

theorem :: ZFMISC_1:44

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

::
:: Intersection of an unordered pair (or a singleton) and a set.
::

theorem :: ZFMISC_1:45

for x being object
for X being set st X /\ {x} = {x} holds
x in X by Lm7;

theorem :: ZFMISC_1:46

for x being object
for X being set st x in X holds
X /\ {x} = {x} by Lm1, XBOOLE_1:28;

theorem :: ZFMISC_1:47

for x, y being object
for Z being set st x in Z & y in Z holds
{x,y} /\ Z = {x,y} by Th31, XBOOLE_1:28;

theorem :: ZFMISC_1:48

for x being object
for X being set st {x} misses X holds
not x in X by Lm5;

theorem Th48: :: ZFMISC_1:49

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

proof end;

theorem :: ZFMISC_1:50

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

theorem Th50: :: ZFMISC_1:51

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

proof end;

theorem :: ZFMISC_1:52

for x being object
for X being set holds
( {x} misses X or {x} /\ X = {x} ) by Lm6, Lm8;

theorem :: ZFMISC_1:53

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

proof end;

theorem :: ZFMISC_1:54

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

proof end;

theorem :: ZFMISC_1:55

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

proof end;

::
:: Difference of an unordered pair (or a singleton) and a set.
::

theorem Th55: :: ZFMISC_1:56

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

proof end;

theorem Th56: :: ZFMISC_1:57

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

proof end;

theorem :: ZFMISC_1:58

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

proof end;

theorem :: ZFMISC_1:59

for x being object
for X being set holds
( {x} \ X = {x} iff not x in X ) by Lm5, Lm6, XBOOLE_1:83;

theorem :: ZFMISC_1:60

for x being object
for X being set holds
( {x} \ X = {} iff x in X ) by Lm1, XBOOLE_1:37;

theorem :: ZFMISC_1:61

for x being object
for X being set holds
( {x} \ X = {} or {x} \ X = {x} ) by Lm9, Lm10;

theorem :: ZFMISC_1:62

for x, y being object
for X being set holds
( {x,y} \ X = {x} iff ( not x in X & ( y in X or x = y ) ) ) by Lm11;

theorem :: ZFMISC_1:63

for x, y being object
for X being set holds
( {x,y} \ X = {x,y} iff ( not x in X & not y in X ) ) by Th48, Th50, XBOOLE_1:83;

theorem Th63: :: ZFMISC_1:64

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

proof end;

theorem :: ZFMISC_1:65

for x, y being object
for 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:66

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

proof end;

::
:: Power Set.
::

theorem :: ZFMISC_1:67

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

proof end;

theorem :: ZFMISC_1:68

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

proof end;

theorem :: ZFMISC_1:69

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

proof end;

theorem :: ZFMISC_1:70

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

proof end;

theorem :: ZFMISC_1:71

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

proof end;

theorem :: ZFMISC_1:72

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

proof end;

theorem :: ZFMISC_1:73

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

proof end;

::
:: Union of a set.
::

theorem :: ZFMISC_1:74

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

theorem :: ZFMISC_1:75

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

theorem :: ZFMISC_1:76

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 Th76: :: ZFMISC_1:77

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

proof end;

theorem :: ZFMISC_1:78

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

proof end;

theorem Th78: :: ZFMISC_1:79

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

proof end;

theorem Th79: :: ZFMISC_1:80

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

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

proof end;

theorem :: ZFMISC_1:82

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

proof end;

theorem :: ZFMISC_1:83

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;

::
:: Cartesian product.
::

theorem Th83: :: ZFMISC_1:84

for z being object
for A, X, Y being set st A c= [:X,Y:] & z in A holds
ex x, y being object st
( x in X & y in Y & z = [x,y] )

proof end;

theorem Th84: :: ZFMISC_1:85

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

proof end;

theorem :: ZFMISC_1:86

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

proof end;

theorem :: ZFMISC_1:87

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

theorem Th87: :: ZFMISC_1:88

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

proof end;

theorem :: ZFMISC_1:89

for X1, X2, Y1, Y2 being set st ( for x, y being object holds
( [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:] ) ) holds
[:X1,Y1:] = [:X2,Y2:]

proof end;

Lm17: for A, B, X1, X2, Y1, Y2 being set st A c= [:X1,Y1:] & B c= [:X2,Y2:] & ( for x, y being object holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B

proof end;

Lm18: for A, B being set st ( for z being object st z in A holds
ex x, y being object st z = [x,y] ) & ( for z being object st z in B holds
ex x, y being object st z = [x,y] ) & ( for x, y being object holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B

proof end;

theorem Th89: :: ZFMISC_1:90

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

proof end;

theorem :: ZFMISC_1:91

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

proof end;

theorem :: ZFMISC_1:92

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

proof end;

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

proof end;

theorem :: ZFMISC_1:93

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

proof end;

theorem :: ZFMISC_1:94

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

proof end;

theorem Th94: :: ZFMISC_1:95

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

proof end;

theorem Th95: :: ZFMISC_1:96

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

proof end;

theorem Th96: :: ZFMISC_1:97

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

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

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

proof end;

theorem Th99: :: ZFMISC_1:100

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

proof end;

theorem :: ZFMISC_1:101

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

proof end;

theorem Th101: :: ZFMISC_1:102

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

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

proof end;

theorem Th103: :: ZFMISC_1:104

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

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

proof end;

theorem :: ZFMISC_1:106

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

proof end;

theorem :: ZFMISC_1:107

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

theorem :: ZFMISC_1:108

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

proof end;

theorem :: ZFMISC_1:109

for x, y being object
for X being set holds
( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )

proof end;

theorem Th109: :: ZFMISC_1:110

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

proof end;

theorem :: ZFMISC_1:111

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

proof end;

theorem :: ZFMISC_1:112

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

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

proof end;

:: from BORSUK_1

theorem Th113: :: ZFMISC_1:114

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

proof end;

:: from ALTCAT_1

theorem :: ZFMISC_1:115

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

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

proof end;

theorem :: ZFMISC_1:117

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

proof end;

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

proof end;

:: from PARTFUN1, 2006.12.05, A.T.

theorem :: ZFMISC_1:119

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

proof end;

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

proof end;

theorem Th119: :: ZFMISC_1:120

for x, y being object
for X being set st not x in X & not y in X holds
X = X \ {x,y}

proof end;

theorem :: ZFMISC_1:121

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

proof end;

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

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

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;

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

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

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

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

:: deftheorem defines are_mutually_distinct ZFMISC_1:def 8 :
for x1, x2, x3, x4, x5, x6 being object holds
( x1,x2,x3,x4,x5,x6 are_mutually_distinct 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 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;

:: deftheorem defines are_mutually_distinct ZFMISC_1:def 9 :
for x1, x2, x3, x4, x5, x6, x7 being object holds
( x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct 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 ) );

:: missing, 2007.02.11, A.T.

theorem :: ZFMISC_1:122

for x1, x2, y1, y2 being object holds [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}

proof end;

:: missing, 2008.03.22, A.T.

theorem :: ZFMISC_1:123

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

:: comp. REALSET1, 2008.07.05, A.T.

definition

let X be set ;

attr X is trivial means :: ZFMISC_1:def 10
for x, y being object 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 object st x in X & y in X holds
x = y );

registration

cluster empty -> trivial for set ;

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

end;

registration

cluster non trivial -> non empty for set ;

coherence
for b₁ being set st not b₁ is trivial holds
not b₁ is empty ;

end;

registration

let x be object ;

cluster {x} -> trivial ;

coherence
{x} is trivial

proof end;

end;

registration

cluster non empty trivial for set ;

existence
ex b₁ being set st
( b₁ is trivial & not b₁ is empty )

proof end;

end;

:: from SPRECT_3, 2008.09.30, A.T.

theorem :: ZFMISC_1:124

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

proof end;

:: from SPRECT_2, 2008.09.30, A.T.

theorem :: ZFMISC_1:125

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

proof end;

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

proof end;

:: from BORSUK_3, 2009.01.24, A.T.

registration

let X be set ;
let Y be empty set ;

cluster [:X,Y:] -> empty ;

coherence
[:X,Y:] is empty by Th89;

end;

registration

let X be empty set ;
let Y be set ;

cluster [:X,Y:] -> empty ;

coherence
[:X,Y:] is empty by Th89;

end;

:: new, 2009.08.26, A.T

theorem :: ZFMISC_1:127

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

proof end;

theorem :: ZFMISC_1:128

for x being object
for B being set st B = [x,{x}] holds
B in [:{x},B:]

proof end;

theorem :: ZFMISC_1:129

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

proof end;

theorem :: ZFMISC_1:130

for A, B being set st B c= A & A is trivial holds
B is trivial

proof end;

registration

cluster non trivial for set ;

existence
not for b₁ being set holds b₁ is trivial

proof end;

end;

theorem Th130: :: ZFMISC_1:131

for X being set st not X is empty & X is trivial holds
ex x being object st X = {x}

proof end;

theorem :: ZFMISC_1:132

for x being set
for X being trivial set st x in X holds
X = {x}

proof end;

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

proof end;

:: Lemma from RELAT_1, FUNCT_4

theorem :: ZFMISC_1:134

for x, y being object
for X being set st [x,y] in X holds
( x in union (union X) & y in union (union X) )

proof end;

theorem Th134: :: ZFMISC_1:135

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

proof end;

theorem :: ZFMISC_1:136

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

proof end;

theorem :: ZFMISC_1:137

for x being object
for Y, X being set holds
( X \/ {x} c= Y iff ( x in Y & X c= Y ) )

proof end;

theorem :: ZFMISC_1:138

for a being object
for A, B being set st A c= B & B c= A \/ {a} & not A \/ {a} = B holds
A = B

proof end;

registration

let A, B be trivial set ;

cluster [:A,B:] -> trivial ;

coherence
[:A,B:] is trivial

proof end;

end;

:: from REALSET1, 2012.08.12, A.T.

theorem :: ZFMISC_1:139

for X being set holds
( not X is trivial iff for x being object holds not X \ {x} is empty )

proof end;

theorem :: ZFMISC_1:140

for X being set holds {X} <> X

proof end;

theorem :: ZFMISC_1:141

for X being set holds bool X <> X

proof end;