:: by Andrzej Trybulec

::

:: Received January 1, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

theorem :: TARSKI:1

canceled;

theorem :: TARSKI:2

definition

let y be set ;

func {y} -> set means :: TARSKI:def 1

for x being set holds

( x in it iff x = y );

correctness

existence

ex b_{1} being set st

for x being set holds

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

uniqueness

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

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

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

b_{1} = b_{2};

;

let z be set ;

func {y,z} -> set means :: TARSKI:def 2

for x being set holds

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

correctness

existence

ex b_{1} being set st

for x being set holds

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

uniqueness

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

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

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

b_{1} = b_{2};

;

commutativity

for b_{1}, y, z being set st ( for x being set holds

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

for x being set holds

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

end;
func {y} -> set means :: TARSKI:def 1

for x being set holds

( x in it iff x = y );

correctness

existence

ex b

for x being set holds

( x in b

uniqueness

for b

( x in b

( x in b

b

;

let z be set ;

func {y,z} -> set means :: TARSKI:def 2

for x being set holds

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

correctness

existence

ex b

for x being set holds

( x in b

uniqueness

for b

( x in b

( x in b

b

;

commutativity

for b

( x in b

for x being set holds

( x in b

:: deftheorem defines { TARSKI:def 1 :

for y, b

( b

( x in b

:: deftheorem defines { TARSKI:def 2 :

for y, z, b

( b

( x in b

theorem :: TARSKI:3

canceled;

theorem :: TARSKI:4

canceled;

definition
end;

:: deftheorem defines c= TARSKI:def 3 :

for X, Y being set holds

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

x in Y );

definition

let X be set ;

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

for x being set holds

( x in it iff ex Y being set st

( x in Y & Y in X ) );

correctness

existence

ex b_{1} being set st

for x being set holds

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

( x in Y & Y in X ) );

uniqueness

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

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

( x in Y & Y in X ) ) ) & ( for x being set 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 set holds

( x in it iff ex Y being set st

( x in Y & Y in X ) );

correctness

existence

ex b

for x being set holds

( x in b

( x in Y & Y in X ) );

uniqueness

for b

( x in b

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

( x in b

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

b

;

:: deftheorem defines union TARSKI:def 4 :

for X, b

( b

( x in b

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

theorem :: TARSKI:5

canceled;

theorem :: TARSKI:6

canceled;

theorem :: TARSKI:7

for x, X being set st x in X holds

ex Y being set st

( Y in X & ( for x being set holds

( not x in X or not x in Y ) ) ) ;

ex Y being set st

( Y in X & ( for x being set holds

( not x in X or not x in Y ) ) ) ;

scheme :: TARSKI:sch 1

Fraenkel{ F_{1}() -> set , P_{1}[ set , set ] } :

Fraenkel{ F

ex X being set st

for x being set holds

( x in X iff ex y being set st

( y in F_{1}() & P_{1}[y,x] ) )

provided
for x being set holds

( x in X iff ex y being set st

( y in F

proof end;

definition

let x, y be set ;

func [x,y] -> set means :: TARSKI:def 5

it = {{x,y},{x}};

correctness

existence

ex b_{1} being set st b_{1} = {{x,y},{x}};

uniqueness

for b_{1}, b_{2} being set st b_{1} = {{x,y},{x}} & b_{2} = {{x,y},{x}} holds

b_{1} = b_{2};

;

end;
func [x,y] -> set means :: TARSKI:def 5

it = {{x,y},{x}};

correctness

existence

ex b

uniqueness

for b

b

;

:: deftheorem defines [ TARSKI:def 5 :

for x, y being set

for b

( b

theorem :: TARSKI:8

canceled;

definition

let X, Y be set ;

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

ex Z being set st

( ( for x being set st x in X holds

ex y being set st

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

ex x being set st

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

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

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

ex Z being set st

( ( for x being set st x in X holds

ex y being set st

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

ex x being set st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being set 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 set st x in X holds

ex y being set st

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

ex x being set st

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

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

theorem :: TARSKI:9

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

ex Z being set st

( Z in M & ( for Y being set st Y c= X holds

Y in Z ) ) ) & ( 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

ex Z being set st

( Z in M & ( for Y being set st Y c= X holds

Y in Z ) ) ) & ( for X being set holds

( not X c= M or X,M are_equipotent or X in M ) ) ) ;