:: Tarski {G}rothendieck Set Theory
:: by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990 Association of Mizar Users

begin

theorem :: TARSKI:1

canceled;

theorem :: TARSKI:2

for X, Y being set st ( for x being set holds
( x in X iff x in Y ) ) holds
X = Y ;

definition

let y be set ;
func {y} -> set means :: TARSKI:def 1
for x being set holds
( x in it iff x = y );
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 ) );
commutativity
for b₁, y, z being set st ( for x being set holds
( x in b₁ iff ( x = y or x = z ) ) ) holds
for x being set holds
( x in b₁ iff ( x = z or x = y ) ) ;

end;

:: deftheorem defines { TARSKI:def 1 :
for y, b₂ being set holds
( b₂ = {y} iff for x being set holds
( x in b₂ iff x = y ) );

:: deftheorem defines { TARSKI:def 2 :
for y, z, b₃ being set holds
( b₃ = {y,z} iff for x being set holds
( x in b₃ iff ( x = y or x = z ) ) );

theorem :: TARSKI:3

canceled;

theorem :: TARSKI:4

canceled;

definition

let X, Y be set ;
pred X c= Y means :: TARSKI:def 3
for x being set st x in X holds
x in Y;

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

end;

:: deftheorem defines union TARSKI:def 4 :
for X, b₂ being set holds
( b₂ = union X iff for x being set holds
( x in b₂ iff ex Y being set st
( 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 ) ) ) ;

scheme :: TARSKI:sch 1
Fraenkel{ F₁() -> set , P₁[ set , set ] } :

ex X being set st
for x being set holds
( x in X iff ex y being set st
( y in F₁() & P₁[y,x] ) )

provided

for x, y, z being set st P₁[x,y] & P₁[x,z] holds
y = z

proof end;

definition

let x, y be set ;
func [x,y] -> set means :: TARSKI:def 5
it = {{x,y},{x}};

end;

:: deftheorem defines [ TARSKI:def 5 :
for x, y being set
for b₃ being set holds
( b₃ = [x,y] iff b₃ = {{x,y},{x}} );

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;

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