:: by Andrzej Trybulec

::

:: Received January 1, 1989

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

begin

theorem :: TARSKI:1

definition

let y be set ;

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 ;

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

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_{2} being set holds

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

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

for y, b

( b

( x in b

:: deftheorem defines { TARSKI:def 2 :

for y, z, b_{3} being set holds

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

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

for y, z, b

( b

( x in b

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

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 ;

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 for x being set holds

( x in it iff ex Y being set st

( x in Y & Y in X ) );

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_{2} being set holds

( b_{2} = union X iff for x being set 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:2

definition

let X, Y be set ;

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

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

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

:: Ueber unerreichbare Kardinalzahlen,

:: Fundamenta Mathematicae, vol. 30 (1938), pp. 68--69

:: Axiom A. (Axiom der unerreichbaren Mengen). Zu jeder Menge N gibt es

:: eine Menge M mit folgenden Eigenschaften:

:: A1. N in M;

:: A2. ist X in M und Y c= X, so ist Y in M;

:: A3. ist X in M und ist Z die Menge, die alle Mengen Y c= X und keine

:: andere Dinge als Element enthaelt, so,ist z in M;

:: A4. ist X c= M und sind dabei die Menge X und M nicht gleichmaechtig,

:: so ist X in M.

:: Alfred Tarski

:: On Well-ordered Subsets of any Set,

:: Fundamenta Mathematicae, vol. 32 (1939), pp. 176--183

:: A. For every set N there exists a system M of sets which satisfies

:: the following conditions:

:: (i) N in M

:: (ii) if X in M and Y c= X, then Y in M

:: (iii) if X in M and Z is the system of all subsets of X, then Z in M

:: (iv) if X c= M and X and M do not have the same potency, then X in M.