Zermelo-Fraenkel set theory (ZF) with Axiom of choice (ZFC)

def. [eqn: x=y ``LRARROW ( FORALL z(z IN x `LRARROW z IN y) WEDGE FORALL w(x IN w `LRARROW y IN w))]

def. [eqn: EXIST !y phi `` LRARROW EXIST t( phi WEDGE FORALL y( phi` RARROW `y=t))]

def. [eqn: x SUBSETEQy`` LRARROW FORALLz(z in x `RARROW z in y)]

1. Axiom of extensionality

[eqn: FORALL x FORALL y(FORALL z (z INx` LRARROW z IN y)RARROW x=y)]

2. Axiom of regularity

[eqn: FORALL x[EXIST a(a in x) RARROW EXISTy(y in x LAND LNOT EXISTz(z in y LANDz in x))]]

3. Axiom schema of specification

for some [eqn: phi (x,w _{1} ,...,w _{n} ,A)]

[eqn: FORALL w _{1} ,w _{2} ,...,w _{n} FORALL A EXIST B` FORALL x(x IN B`` LRARROW (x IN A WEDGE phi))]

def. [eqn: LEFT { x IN A: phi RIGHT } :=B`( FORALL x(x IN B`` LRARROW (x IN A WEDGE phi )))]

def. [eqn: EMPTYSET := LEFT { x IN y:x NOTIN y RIGHT }]

4. Axiom of pairing

[eqn: FORALL x FORALL y EXIST z(x in z LAND y in z)]

def. [eqn: left{ w right}:=left{x in z:x=w right}]

def. [eqn: (a,b)=left{left{a right},left{a,b right}right}]

def. [eqn: (a _{1} ,a _{2} ,...,a _{n} ,b):= LEFT { LEFT { (a _{1} ,...,a _{n} ) RIGHT } , LEFT { (a _{1} ,...,a _{n} ),b RIGHT } RIGHT }]

5. Axiom of union

[eqn: FORALL]F[eqn: EXIST A FORALL Y` FORALL x[(x IN Y` WEDGE Y` IN]F[eqn: ) RARROW `x IN A]]

def. [eqn: cup]F[eqn: := LEFT { x IN A: EXIST Y(x IN Y WEDGE Y IN RIGHT .]F[eqn: left. )right}]

6. Axiom schema of replacement

for some [eqn: phi (x,y,w _{1} ,...,w _{n} ,A)]

[eqn: FORALL A FORALL w _{1} ,w _{2} ,...,w _{n} [ FORALL x(x IN a RARROW EXIST !y phi ) RARROW EXIST B FORALL x(x IN A RARROW EXIST y(y IN B WEDGE phi ))]]

7. Axiom of infinity

[eqn: EXIST X[ EMPTYSET IN X WEDGE FORALL y(y IN X RARROW y CUP LEFT { y RIGHT } IN X)]]

def. [eqn: ℕ:= LEFT { x IN X _{1} : FORALL X(x IN X) WEDGE x != EMPTYSET RIGHT }]

8. Axiom of power set

[eqn: FORALL x EXIST y FORALLz[z SUBSETEQ x RARROW z in y]]

def. P[eqn: (x):= LEFT { z IN y:z SUBSETEQ x RIGHT }]

9. Well-ordering theorem (Axiom of choice)

def. [eqn: (R] well-orders [eqn: x) LRARROW R( FORALL a IN x FORALL b IN x FORALL c IN x[(R(a,b) WEDGE R(b,a) RARROW a=b)# ~~~~~~ WEDGE (R(a,b) WEDGE R(b,c) RARROW R(a,c)) WEDGE (R(a,b) LOR R(b,a))]# ~~~~~~ WEDGE [ FORALL Y SUBSETEQ X(Y != EMPTYSET RARROW EXIST !y IN Y[ FORALL z IN YR(y,z)])])]

[eqn: FORALL x EXIST R(R` rm] well-orders [eqn: x)]

[eqn: LRARROW FORALL x[ EMPTYSET NOTIN x RARROW EXIST f( FORALL y IN x(f(y) IN y))]]

Neumann Ordinals

def. [eqn: 0:= LEFT { EMPTYSET RIGHT }]

def. [eqn: S(a):=a CUP LEFT { a RIGHT }]

def. [eqn: 1:=S(0)]

def. [eqn: n<= m LRARROW`n SUBSETEQm,~n>= m LRARROW`n SUPSETEQ m]

def. [eqn: +:( FORALL n IN (ℕ CUP LEFT { 0 RIGHT } )(n+1=S(n)) WEDGE FORALL n FORALL m FORALL l[(n+m)+l=n+(m+l)# ~~~ WEDGE n+m=m+n])]

def. [eqn: -:( FORALL n FORALL m[(-n)+n=0 WEDGE -(n+m)=(-n)+(-m)])]

def. [eqn: S ^{-1} (n):=n-1]

def. [eqn: TIMES :( FORALL n FORALL m(n TIMES S(m)=n TIMES m+n WEDGE n TIMES S ^{-1} (m)=n TIMES m-m land n times 0 = 0)]