:: Some Basic Properties of Sets
:: by Czes{\l}aw Byli\'nski
::
:: Copyright (c) 1990-2012 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 S1[ 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 b1 being set st for Z being set holds ( Z in b1 iff Z c= X ) proof end; uniqueness for b1, b2 being set st ( for Z being set holds ( Z in b1 iff Z c= X ) ) & ( for Z being set holds ( Z in b2 iff Z c= X ) ) holds b1 = b2 proof end; end; :: 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] ) )
proof end;
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
proof end;
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] ) ) );

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

::
:: Empty set.
::
theorem :: ZFMISC_1:1
proof end;

theorem :: ZFMISC_1:2
proof end;

::
:: Singleton and unordered pairs.
::
theorem Th3: :: ZFMISC_1:3
for x, y being set st {x} c= {y} holds
x = y
proof end;

theorem Th4: :: ZFMISC_1:4
for x, y1, y2 being set st {x} = {y1,y2} holds
x = y1
proof end;

theorem :: ZFMISC_1:5
for x, y1, y2 being set st {x} = {y1,y2} holds
y1 = y2
proof end;

theorem Th6: :: ZFMISC_1:6
for x1, x2, y1, y2 being set holds
( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 )
proof end;

theorem Th7: :: ZFMISC_1:7
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:8
for x, y being set st {x} \/ {y} = {x} holds
x = y
proof end;

theorem :: ZFMISC_1:9
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:10
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 Th11: :: ZFMISC_1:11
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:12
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}

by ;

theorem :: ZFMISC_1:13
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 )

by ;

theorem :: ZFMISC_1:14
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 )

by ;

theorem :: ZFMISC_1:15
for x, y being set st {x} \ {y} = {} holds
x = y
proof end;

theorem :: ZFMISC_1:16
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:17
for x, y being set st x <> y holds
{x,y} \ {y} = {x}
proof end;

theorem :: ZFMISC_1:18
for x, y being set st {x} c= {y} holds
x = y by Th3;

theorem :: ZFMISC_1:19
for z, x, y being set holds
( not {z} c= {x,y} or z = x or z = y )
proof end;

theorem Th20: :: ZFMISC_1:20
for x, y, z being set st {x,y} c= {z} holds
x = z
proof end;

theorem :: ZFMISC_1:21
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:22
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:23
for x, y being set st x <> y holds
{x} \+\ {y} = {x,y}
proof end;

theorem :: ZFMISC_1:24
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:25
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:26
for x, y being set holds union {{x},{y}} = {x,y}
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:27
canceled;

theorem :: ZFMISC_1:28
for x, y, x1, y1 being set holds
( [x,y] in [:{x1},{y1}:] iff ( x = x1 & y = y1 ) )
proof end;

theorem :: ZFMISC_1:29
for x, y being set holds [:{x},{y}:] = {[x,y]}
proof end;

theorem Th30: :: ZFMISC_1:30
for x, y, z being set 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, X being set holds
( {x} c= X iff x in X ) by Lm1;

theorem Th32: :: ZFMISC_1:32
for x1, x2, 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 Y, x being set holds
( Y c= {x} iff ( Y = {} or Y = {x} ) ) by Lm3;

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

theorem :: ZFMISC_1:35
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:36
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;

::
:: Sum of an unordered pair (or a singleton) and a set.
::
theorem Th37: :: ZFMISC_1:37
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:38
for z, X, Y being set st {z} = X \/ Y & X <> Y & not X = {} holds
Y = {}
proof end;

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

theorem :: ZFMISC_1:40
for x, X being set st x in X holds
{x} \/ X = X by ;

theorem :: ZFMISC_1:41
for x, y, Z being set st {x,y} \/ Z c= Z holds
x in Z
proof end;

theorem :: ZFMISC_1:42
for x, Z, y being set st x in Z & y in Z holds
{x,y} \/ Z = Z by ;

theorem :: ZFMISC_1:43
for x, X being set holds {x} \/ X <> {} ;

theorem :: ZFMISC_1:44
for x, y, X being set holds {x,y} \/ X <> {} ;

::
:: Intersection of an unordered pair (or a singleton) and a set.
::
theorem :: ZFMISC_1:45
for X, x being set st X /\ {x} = {x} holds
x in X by Lm8;

theorem :: ZFMISC_1:46
for x, X being set st x in X holds
X /\ {x} = {x} by ;

theorem :: ZFMISC_1:47
for x, Z, y being set st x in Z & y in Z holds
{x,y} /\ Z = {x,y} by ;

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

theorem Th49: :: ZFMISC_1:49
for x, y, Z being set st {x,y} misses Z holds
not x in Z
proof end;

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

theorem Th51: :: ZFMISC_1:51
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:52
for x, X being set holds
( {x} misses X or {x} /\ X = {x} ) by ;

theorem :: ZFMISC_1:53
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:54
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:55
for x, y, 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 Th56: :: ZFMISC_1:56
for z, X, x being set holds
( z in X \ {x} iff ( z in X & z <> x ) )
proof end;

theorem Th57: :: ZFMISC_1:57
for X, x being set holds
( X \ {x} = X iff not x in X )
proof end;

theorem :: ZFMISC_1:58
for X, x being set holds
( not X \ {x} = {} or X = {} or X = {x} )
proof end;

theorem :: ZFMISC_1:59
for x, X being set holds
( {x} \ X = {x} iff not x in X ) by ;

theorem :: ZFMISC_1:60
for x, X being set holds
( {x} \ X = {} iff x in X ) by ;

theorem :: ZFMISC_1:61
for x, X being set holds
( {x} \ X = {} or {x} \ X = {x} ) by ;

theorem :: ZFMISC_1:62
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:63
for x, y, X being set holds
( {x,y} \ X = {x,y} iff ( not x in X & not y in X ) ) by ;

theorem Th64: :: ZFMISC_1:64
for x, y, X being set holds
( {x,y} \ X = {} iff ( x in X & y in X ) )
proof end;

theorem :: ZFMISC_1:65
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:66
for X, x, y 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 X, A being set st X in A holds
X c= union A by Lm15;

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

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 Th77: :: 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) = () \/ ()
proof end;

theorem Th79: :: ZFMISC_1:79
for A, B being set holds union (A /\ B) c= () /\ ()
proof end;

theorem Th80: :: 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 ()
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) = () /\ ()
proof end;

::
:: Cartesian product.
::
theorem Th84: :: ZFMISC_1:84
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 Th85: :: ZFMISC_1:85
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:86
for X, Y being set holds [:X,Y:] c= bool (bool (X \/ Y))
proof end;

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

theorem Th88: :: ZFMISC_1:88
for x, y, X, Y being set st [x,y] in [:X,Y:] holds
[y,x] in [:Y,X:]
proof end;

theorem :: ZFMISC_1:89
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 Th90: :: 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;

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:93
for X being set st X c= [:X,X:] holds
X = {}
proof end;

theorem :: ZFMISC_1:94
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 Th95: :: 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 Th96: :: ZFMISC_1:96
for X1, Y1, X2, Y2 being set st X1 c= Y1 & X2 c= Y2 holds
[:X1,X2:] c= [:Y1,Y2:]
proof end;

theorem Th97: :: 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 Th100: :: 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, X, B, Y being set st A c= X & B c= Y holds
[:A,Y:] /\ [:X,B:] = [:A,B:]
proof end;

theorem Th102: :: 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 Th104: :: 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, Y being set holds
( [x,y] in [:{z},Y:] iff ( x = z & y in Y ) )
proof end;

theorem :: ZFMISC_1:106
for x, y, X, z being set holds
( [x,y] in [:X,{z}:] iff ( x in X & y = z ) )
proof end;

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

theorem :: ZFMISC_1:108
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:109
for x, y, X being set holds
( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )
proof end;

theorem Th110: :: ZFMISC_1:110
for X1, Y1, X2, 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, 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

:: from BORSUK_1
theorem Th114: :: 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, X being set st x in X holds
(X \ {x}) \/ {x} = X
proof end;

theorem :: ZFMISC_1:117
for x, 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, 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 Th120: :: ZFMISC_1:120
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:121
for x, y, 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 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 ) );

:: from CARD_2, 2007.01.18. AK
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 ) );

:: from BORSUK_5, 2007.01.18. AK
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 ) );

:: missing, 2007.02.11, A.T.
theorem :: ZFMISC_1:122
for x1, x2, y1, y2 being set 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, A being set st x <> y holds
(A \/ {x}) \ {y} = (A \ {y}) \/ {x} by ;

:: comp. REALSET1, 2008.07.05, A.T.
definition
let X be set ;
attr X is trivial means :Def10: :: ZFMISC_1:def 10
for x, y being set st x in X & y in X holds
x = y;
end;

:: deftheorem Def10 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 for set ;
coherence
for b1 being set st b1 is empty holds
b1 is trivial
proof end;
end;

registration
cluster non trivial -> non empty for set ;
coherence
for b1 being set st not b1 is trivial holds
not b1 is empty
;
end;

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

registration
cluster non empty trivial for set ;
existence
ex b1 being set st
( b1 is trivial & not b1 is empty )
proof end;
end;

:: from SPRECT_3, 2008.09.30, A.T.
theorem :: ZFMISC_1:124
for A, B, C, p being set 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 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: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 Th90;
end;

registration
let X be empty set ;
let Y be set ;
cluster [:X,Y:] -> empty ;
coherence
[:X,Y:] is empty
by Th90;
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 set holds [x,{x}] in [:{x},[x,{x}]:]
proof end;

theorem :: ZFMISC_1:129
for B, A being set st B in [:A,B:] holds
ex x being set st
( x in A & B = [x,{x}] )
proof end;

theorem :: ZFMISC_1:130
for B, A being set st B c= A & A is trivial holds
B is trivial
proof end;

registration
cluster non trivial for set ;
existence
not for b1 being set holds b1 is trivial
proof end;
end;

theorem Th131: :: ZFMISC_1:131
for X being set st not X is empty & X is trivial holds
ex x being set 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, X being set st [x,y] in X holds
( x in union () & y in union () )
proof end;

theorem Th135: :: ZFMISC_1:135
for Y, x, 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, X being set holds
( x in X \/ {y} iff ( x in X or x = y ) )
proof end;

theorem :: ZFMISC_1:137
for x, Y, X being set holds
( X \/ {x} c= Y iff ( x in Y & X c= Y ) )
proof end;

theorem :: ZFMISC_1:138
for A, B, a being set st A c= B & B c= A \/ {a} & not A \/ {a} = B holds
A = B
proof end;