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