:: by Andrzej Trybulec

::

:: Received January 1, 1989

:: Copyright (c) 1990-2021 Association of Mizar Users

theorem :: TARSKI:2

definition

let y be object ;

existence

ex b_{1} being set st

for x being object holds

( x in b_{1} iff x = y )

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

( x in b_{1} iff x = y ) ) & ( for x being object holds

( x in b_{2} iff x = y ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ( x = y or x = z ) )
by TARSKI_0:3;

uniqueness

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

( x in b_{1} iff ( x = y or x = z ) ) ) & ( for x being object holds

( x in b_{2} iff ( x = y or x = z ) ) ) holds

b_{1} = b_{2}

for b_{1} being set

for y, z being object st ( for x being object holds

( x in b_{1} iff ( x = y or x = z ) ) ) holds

for x being object holds

( x in b_{1} iff ( x = z or x = y ) )
;

end;
existence

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

let z be object ;
func {y,z} -> set means :Def2: :: TARSKI:def 2

for x being object holds

( x in it iff ( x = y or x = z ) );

existence for x being object holds

( x in it iff ( x = y or x = z ) );

ex b

for x being object holds

( x in b

uniqueness

for b

( x in b

( x in b

b

proof end;

commutativity for b

for y, z being object st ( for x being object holds

( x in b

for x being object holds

( x in b

:: deftheorem defines { TARSKI:def 1 :

for y being object

for b_{2} being set holds

( b_{2} = {y} iff for x being object holds

( x in b_{2} iff x = y ) );

for y being object

for b

( b

( x in b

:: deftheorem Def2 defines { TARSKI:def 2 :

for y, z being object

for b_{3} being set holds

( b_{3} = {y,z} iff for x being object holds

( x in b_{3} iff ( x = y or x = z ) ) );

for y, z being object

for b

( b

( x in b

definition
end;

:: deftheorem defines c= TARSKI:def 3 :

for X, Y being set holds

( X c= Y iff for x being object st x in X holds

x in Y );

for X, Y being set holds

( X c= Y iff for x being object st x in X holds

x in Y );

definition

let X be set ;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex Y being set st

( x in Y & Y in X ) ) by TARSKI_0:4;

uniqueness

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

( x in b_{1} iff ex Y being set st

( x in Y & Y in X ) ) ) & ( for x being object holds

( x in b_{2} iff ex Y being set st

( x in Y & Y in X ) ) ) holds

b_{1} = b_{2}

end;
func union X -> set means :: TARSKI:def 4

for x being object holds

( x in it iff ex Y being set st

( x in Y & Y in X ) );

existence for x being object holds

( x in it iff ex Y being set st

( x in Y & Y in X ) );

ex b

for x being object holds

( x in b

( x in Y & Y in X ) ) by TARSKI_0:4;

uniqueness

for b

( x in b

( x in Y & Y in X ) ) ) & ( for x being object holds

( x in b

( x in Y & Y in X ) ) ) holds

b

proof end;

:: deftheorem defines union TARSKI:def 4 :

for X, b_{2} being set holds

( b_{2} = union X iff for x being object holds

( x in b_{2} iff ex Y being set st

( x in Y & Y in X ) ) );

for X, b

( b

( x in b

( x in Y & Y in X ) ) );

theorem :: TARSKI:3

definition

let x, X be set ;

:: original: in

redefine pred x in X;

asymmetry

for x, X being set st R2(b_{1},b_{2}) holds

not R2(b_{2},b_{1})

end;
:: original: in

redefine pred x in X;

asymmetry

for x, X being set st R2(b

not R2(b

proof end;

definition

let X, Y be set ;

end;
pred X,Y are_equipotent means :: TARSKI:def 6

ex Z being set st

( ( for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) );

ex Z being set st

( ( for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) );

:: deftheorem defines are_equipotent TARSKI:def 6 :

for X, Y being set holds

( X,Y are_equipotent iff ex Z being set st

( ( for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) ) );

for X, Y being set holds

( X,Y are_equipotent iff ex Z being set st

( ( for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) ) );