Theory ZFC_Rudiments

section ‹Some rudiments of ZFC›

text ‹See also 🌐‹https://www.isa-afp.org/entries/ZFC_in_HOL.html› by L.C. Paulson.›

theory ZFC_Rudiments
  imports Main
begin

typedecl V

axiomatization elts :: "V ⇒ V set"
 where ext [intro?]:    "elts x = elts y ⟹ x=y"
   and down_raw:        "Y ⊆ elts x ⟹ Y ∈ range elts"
   and Union_raw:       "X ∈ range elts ⟹ Union (elts ` X) ∈ range elts"
   and Pow_raw:         "X ∈ range elts ⟹ inv elts ` Pow X ∈ range elts"
   and replacement_raw: "X ∈ range elts ⟹ f ` X ∈ range elts"
   and inf_raw:         "range (g :: nat ⇒ V) ∈ range elts"
   and foundation:      "wf {(x,y). x ∈ elts y}"

definition small :: "'a set ⇒ bool" 
  where "small X ≡ ∃V_of :: 'a ⇒ V. inj_on V_of X ∧ V_of ` X ∈ range elts"

definition set :: "V set ⇒ V"
  where "set X ≡ (if small X then inv elts X else inv elts {})"

definition VPow :: "V ⇒ V"
  where "VPow x = set (set ` Pow (elts x))"

definition vpair :: "V ⇒ V ⇒ V"
  where "vpair a b = set {set {a},set {a,b}}"

definition vfst :: "V ⇒ V"
  where "vfst p = (THE x. ∃y. p = vpair x y)"

definition vsnd :: "V ⇒ V"
  where "vsnd p = (THE y. ∃x. p = vpair x y)"

definition VSigma :: "V ⇒ (V ⇒ V) ⇒ V"
  where "VSigma A B = set(⋃x ∈ elts A. ⋃y ∈ elts (B x). {vpair x y})"

abbreviation vtimes :: "V ⇒ V ⇒ V"
  where "vtimes A B ≡ VSigma A (λx. B)"

definition pairs :: "V ⇒ (V × V) set"
  where "pairs r = {(x,y). vpair x y ∈ elts r}"

definition VLambda :: "V ⇒ (V ⇒ V) ⇒ V"
  where "VLambda A b = set ((λx. vpair x (b x)) ` elts A)"

definition app :: "V ⇒ V ⇒ V"
  where "app f x ≡ THE y. vpair x y ∈ elts f"

definition VPi :: "V ⇒ (V ⇒ V) ⇒ V"
  where "VPi A B =
    set {f ∈ elts (VPow (VSigma A B)). elts A ⊆ Domain (pairs f) ∧ single_valued (pairs f)}"

end