B.1 TARSKI

Tarski Grothendieck Set Theory by Andrzej Trybulec

reserve x,y,z,u,N,M,X,Y,Z for set;

2 (for x holds x in X iff x in Y) implies X = Y;

def 1 func { y } means x in it iff x = y;

def 2 func { y, z } means x in it iff x = y or x = z;

def 3 pred X c= Y means x in X implies x in Y;

def 4 func union X means x in it iff ex Y st x in Y & Y in X;

7 x in X implies ex Y st Y in X & not ex x st x in X & x in Y;

scheme Fraenkel { A()-> set, P[set, set] }:

ex X st for x holds x in X iff ex y st y in A() & P[y,x]

provided for x,y,z st P[x,y] & P[x,z] holds y = z;

def 5 func [x,y] equals { { x,y }, { x } };

def 6 pred X,Y are_equipotent means

ex Z st

(for x st x in X ex y st y in Y & [x,y] in Z) &

(for y st y in Y ex x st x in X & [x,y]
in Z) &

for x,y,z,u st [x,y] in Z & [z,u] in Z holds
x = z iff y = u;

9 ex M st N in M &

(for X,Y holds X in M & Y c= X implies Y in M) &

(for X st X in M ex Z st Z in M & for Y st Y c= X holds
Y in Z) &

(for X holds X c= M implies X,M are_equipotent or X in M);