B.1 TARSKI

TARSKI. ABS (Digest)
Tarski Grothendieck Set Theory, by Andrzej Trybulec.

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

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

def 1 func { y } -> non empty;
def 2 func { y, z } -> set means x C it iff x = y or x = z;

cluster { y } -> non empty;
cluster { y, z } -> non empty;

def 3 pred X c= Y means x C X implies x C Y;
def 4 func union X -> set means x C it iff ex Y st x C Y & Y C X;

6 X = bool Y iff for Z holds Z C X iff Z c= Y;
7 x C X implies ex Y st Y C X & not ex x st x C X & x C Y;

scheme fraenkel { A( )-> set, P[Any, Any] }:
ex X st for x holds x C X iff ex y st y C A ( ) & P[y, x]
provided for x,y,z st P[x,y] & P[x,z] holds y = z;

def 5 func [x,y] means it = { { x,y }, {x} };

8 [ x, y ] = { { x, y }, {x} };

def 6 pred X = Y means

ex Z st
(for x st x C X ex y st y C Y & [x,y] C Z) &
(for y st y C Y ex x st x C X & [x,y] C Z) &
for x, y, z, u st [x,y] C Z & [z,u] C Z holds x = z iff y=u;

9 ex M st N C M &

(for X, Y holds X C M & Y c= X implies Y C M) &
(for X holds X C M implies bool X C M)&
(for X holds X c= M implies X = M or X C M);