set.mm0

delimiter $ ( ) ~ { } $;
strict provable sort wff;
term wi (ph ps: wff): wff; infixr wi: $->$ prec 25;
term wn (ph: wff): wff; prefix wn: $~$ prec 40;

axiom ax_1 (ph ps: wff): $ ph -> ps -> ph $;
axiom ax_2 (ph ps ch: wff): $ (ph -> ps -> ch) -> (ph -> ps) -> ph -> ch $;
axiom ax_3 (ph ps: wff): $ (~ph -> ~ps) -> ps -> ph $;
axiom ax_mp (ph ps: wff): $ ph $ > $ ph -> ps $ > $ ps $;

theorem a1i (ph ps: wff): $ ph $ > $ ps -> ph $;

def wb (ph ps: wff): wff = $ ~((ph -> ps) -> ~(ps -> ph)) $;
infixl wb: $<->$ prec 20;

theorem bi1 (ph ps: wff): $ (ph <-> ps) -> ph -> ps $;
theorem bi2 (ph ps: wff): $ (ph <-> ps) -> ps -> ph $;
theorem bi3 (ph ps: wff): $ (ph -> ps) -> (ps -> ph) -> (ph <-> ps) $;

def wa (ph ps: wff): wff = $ ~(ph -> ~ps) $;
infixl wa: $/\$ prec 20;
theorem df_an (ph ps: wff): $ (ph /\ ps) <-> ~(ph -> ~ps) $;

term wtru: wff; prefix wtru: $T.$ prec max;
axiom tru: $ T. $;
theorem df_tru (ph: wff): $ T. <-> (ph <-> ph) $;

pure sort set;
term wal {x: set} (ph: wff x): wff; prefix wal: $A.$ prec 30;

def wex {x: set} (ph: wff x): wff = $ ~(A. x ~ph) $;
prefix wex: $E.$ prec 30;
theorem df_ex {x: set} (ph: wff x): $ E. x ph <-> ~(A. x ~ph) $;

axiom ax_gen {x: set} (ph: wff x): $ ph $ > $ A. x ph $;
axiom ax_4 {x: set} (ph ps: wff x): $ A. x (ph -> ps) -> A. x ph -> A. x ps $;
axiom ax_5 {x: set} (ph: wff): $ ph -> A. x ph $;

term weq (a b: set): wff; infixl weq: $=s$ prec 50;
term wel (a b: set): wff; infixl wel: $es.$ prec 40;

def weu {x .y: set} (ph: wff x): wff = $ E. y A. x (ph <-> x =s y) $;
prefix weu: $E!$ prec 30;
theorem df_eu {x y: set} (ph: wff x):
  $ E! x ph <-> E. y A. x (ph <-> x =s y) $;

axiom ax_6 {x: set} (a: set): $ E. x x =s a $;
axiom ax_7 (a b c: set): $ a =s b -> a =s c -> b =s c $;

axiom ax_8 (a b c: set): $ a =s b -> a es. c -> b es. c $;
axiom ax_9 (a b c: set): $ a =s b -> c es. a -> c es. b $;

axiom ax_10 {x: set} (ph: wff x): $ ~(A. x ph) -> A. x ~(A. x ph) $;
axiom ax_11 {x y: set} (ph: wff x y): $ A. x A. y ph -> A. y A. x ph $;
axiom ax_12 {x y: set} (ph: wff y): $ A. y ph -> A. x (x =s y -> ph) $;

axiom ax_ext {x: set} (a b: set): $ A. x (x es. a <-> x es. b) -> a =s b $;
axiom ax_rep {x y z: set} (a: set) (ph: wff y z):
  $ A. y E. x A. z (ph -> z =s x) ->
    E. x A. z (z es. x <-> E. y (y es. a /\ ph)) $;
axiom ax_pow {x y z: set} (a: set):
  $ E. x A. y (A. z (z es. y -> z es. a) -> y es. x) $;
axiom ax_un {x y z: set} (a: set):
  $ E. x A. y (E. z (y es. z /\ z es. a) -> y es. x) $;
axiom ax_reg {x y: set} (a: set):
  $ E. x x es. a -> E. x (x es. a /\ A. y (y es. x -> ~ y es. a)) $;
axiom ax_inf {x: set} (a: set) {y z: set}:
  $ E. x (a es. x /\ A. y (y es. x -> E. z (y es. z /\ z es. x))) $;
axiom ax_ac {x y: set} (a: set) {z w: set}:
  $ E. x A. y (y es. a -> E. z z es. y ->
    E! z (z es. y /\ E. w (w es. x /\ y es. w /\ z es. w))) $;

strict sort class;
term cab {x: set} (ph: wff x): class;
term welc (a: set) (A: class): wff; infixl welc: $ec.$ prec 50;
notation cab {x: set} (ph: wff x): class = (${$:max) x ($|$:0) ph ($}$:0);

axiom ax_8b (a b: set) (A: class): $ a =s b -> a ec. A -> b ec. A $;

axiom ax_clab {x: set} (ph: wff x): $ x ec. {x | ph} <-> ph $;

def wceq {.x: set} (A B: class): wff = $ A. x (x ec. A <-> x ec. B) $;
infixl wceq: $=$ prec 50;

def cv {.x: set} (a: set): class = $ {x | x es. a} $;
coercion cv: set > class;

def wcel {.x: set} (A B: class): wff = $ E. x (x = A /\ x ec. B) $;
infixl wcel: $e.$ prec 50;