:: 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_{1}[ set ] means $1 c= X;

existence

ex b_{1} being set st

for Z being set holds

( Z in b_{1} iff Z c= X )

for b_{1}, b_{2} being set st ( for Z being set holds

( Z in b_{1} iff Z c= X ) ) & ( for Z being set holds

( Z in b_{2} iff Z c= X ) ) holds

b_{1} = b_{2}

end;
defpred S

existence

ex b

for Z being set holds

( Z in b

proof end;

uniqueness for b

( Z in b

( Z in b

b

proof end;

:: deftheorem Def1 defines bool ZFMISC_1:def 1 :

for X, b_{2} being set holds

( b_{2} = bool X iff for Z being set holds

( Z in b_{2} iff Z c= X ) );

for X, b

( b

( Z in b

definition

let X1, X2 be set ;

defpred S_{1}[ object ] means ex x, y being object st

( x in X1 & y in X2 & $1 = [x,y] );

ex b_{1} being set st

for z being object holds

( z in b_{1} iff ex x, y being object st

( x in X1 & y in X2 & z = [x,y] ) )

for b_{1}, b_{2} being set st ( for z being object holds

( z in b_{1} iff ex x, y being object st

( x in X1 & y in X2 & z = [x,y] ) ) ) & ( for z being object holds

( z in b_{2} iff ex x, y being object st

( x in X1 & y in X2 & z = [x,y] ) ) ) holds

b_{1} = b_{2}

end;
defpred S

( 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 for z being object holds

( z in it iff ex x, y being object st

( x in X1 & y in X2 & z = [x,y] ) );

ex b

for z being object holds

( z in b

( x in X1 & y in X2 & z = [x,y] ) )

proof end;

uniqueness for b

( z in b

( x in X1 & y in X2 & z = [x,y] ) ) ) & ( for z being object holds

( z in b

( x in X1 & y in X2 & z = [x,y] ) ) ) holds

b

proof end;

:: deftheorem Def2 defines [: ZFMISC_1:def 2 :

for X1, X2, b_{3} being set holds

( b_{3} = [:X1,X2:] iff for z being object holds

( z in b_{3} iff ex x, y being object st

( x in X1 & y in X2 & z = [x,y] ) ) );

for X1, X2, b

( b

( z in b

( x in X1 & y in X2 & z = [x,y] ) ) );

:: deftheorem defines [: ZFMISC_1:def 3 :

for X1, X2, X3 being set holds [:X1,X2,X3:] = [:[:X1,X2:],X3:];

for X1, X2, X3 being set holds [:X1,X2,X3:] = [:[:X1,X2:],X3:];

:: deftheorem defines [: ZFMISC_1:def 4 :

for X1, X2, X3, X4 being set holds [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:];

for X1, X2, X3, X4 being set holds [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:];

::

:: Singleton and unordered pairs.

::

:: Singleton and unordered pairs.

::

Lm4: for x being object

for X being set st {x} \/ X c= X holds

x in X

proof end;

Lm5: for x being object

for X being set st {x} misses X holds

not x in X

proof end;

Lm6: for x being object

for X being set st not x in X holds

{x} misses X

proof end;

Lm7: for x being object

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

x in X

proof end;

Lm8: for x being object

for X being set st x in X holds

X /\ {x} = {x}

by Lm1, XBOOLE_1:28;

Lm9: for x being object

for X being set holds

( {x} \ X = {x} iff not x in X )

by Lm5, Lm6, XBOOLE_1:83;

Lm10: for x being object

for X being set holds

( {x} \ X = {} iff x in X )

by Lm1, XBOOLE_1:37;

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;

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;

Lm14: for A, X being set st X in A holds

X c= union A

by TARSKI:def 4;

Lm15: for X, Y being set 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;

::$CT

::

:: Singleton and unordered pairs included in a set.

::

:: Singleton and unordered pairs included in a set.

::

::

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

::

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

::

theorem :: ZFMISC_1:33

theorem :: ZFMISC_1:34

theorem :: ZFMISC_1:35

theorem :: ZFMISC_1:36

::

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

::

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

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

theorem :: ZFMISC_1:42

::

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

::

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

::

theorem :: ZFMISC_1:46

theorem :: ZFMISC_1:47

theorem :: ZFMISC_1:52

::

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

::

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

::

theorem :: ZFMISC_1:59

theorem :: ZFMISC_1:60

theorem :: ZFMISC_1:61

theorem :: ZFMISC_1:62

theorem :: ZFMISC_1:63

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

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

for X being set holds

( X \ {x,y} = {} iff ( X = {} or X = {x} or X = {y} or X = {x,y} ) )

proof end;

::

:: Power Set.

::

:: Power Set.

::

::

:: Union of a set.

::

:: Union of a set.

::

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)

X misses Y ) holds

union (A /\ B) = (union A) /\ (union B)

proof end;

::

:: Cartesian product.

::

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

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 )

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

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

( [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;

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

( [:(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:] )

( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] & [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )

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

( [:(X \ Y),Z:] = [:X,Z:] \ [:Y,Z:] & [:Z,(X \ Y):] = [:Z,X:] \ [:Z,Y:] )

proof end;

theorem :: ZFMISC_1:107

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

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

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 )

( X1 = X2 & Y1 = Y2 )

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

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

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 )

( 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

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

B c= D

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

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

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;

:: from INCPROJ, 2007.01.18. AK

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

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 ;

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

( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 );

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

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

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

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

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

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 ;

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

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

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

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.

:: missing, 2008.03.22, A.T.

theorem :: ZFMISC_1:123

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

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

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

:: from SPRECT_3, 2008.09.30, A.T.

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

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

x misses y ) holds

union A misses union B

proof end;

:: from BORSUK_3, 2009.01.24, A.T.

registration
end;

registration
end;

:: new, 2009.08.26, A.T

registration
end;

:: from JORDAN16, 2011.04.27, A.T.

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

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

( x in union (union X) & y in union (union X) )

proof end;

registration
end;

:: from REALSET1, 2012.08.12, A.T.

:: Empty set.

::