@[reducible, inline]

abbrev InaccessibleCardinal : Type (u_1 + 1)

Equations

• InaccessibleCardinal = { κ : Cardinal.{?u.3} // κ.IsInaccessible }

def SecondOrder.Language.zf : Language

Equations

• SecondOrder.Language.zf = { Func := SecondOrder.Language.zf.Func✝, Rel := SecondOrder.Language.zf.Rel✝ }

instance SecondOrder.Language.zf.instEmptyCollectionTerm {l : List Ty} : EmptyCollection (zf.Term l)

Equations

• SecondOrder.Language.zf.instEmptyCollectionTerm = { emptyCollection := SecondOrder.Language.zf.Func.empty✝ ⬝ᶠ []ᵥ }

instance SecondOrder.Language.zf.instInsertTerm {l : List Ty} : Insert (zf.Term l) (zf.Term l)

Equations

• SecondOrder.Language.zf.instInsertTerm = { insert := fun (x1 x2 : SecondOrder.Language.zf.Term l) => SecondOrder.Language.zf.Func.insert✝ ⬝ᶠ [x1, x2]ᵥ }

def SecondOrder.Language.zf.sUnion {l : List Ty} (t : zf.Term l) : zf.Term l

Equations

• SecondOrder.Language.zf.sUnion t = SecondOrder.Language.zf.Func.sUnion✝ ⬝ᶠ [t]ᵥ

def SecondOrder.Language.zf.«term⋃₀_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def SecondOrder.Language.zf.powerset {l : List Ty} (t : zf.Term l) : zf.Term l

Equations

• SecondOrder.Language.zf.powerset t = SecondOrder.Language.zf.Func.powerset✝ ⬝ᶠ [t]ᵥ

def SecondOrder.Language.zf.term𝓟_ : Lean.ParserDescr

Equations

• SecondOrder.Language.zf.term𝓟_ = Lean.ParserDescr.node `SecondOrder.Language.zf.term𝓟_ 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓟") (Lean.ParserDescr.cat `term 100))

def SecondOrder.Language.zf.omega {l : List Ty} : zf.Term l

Equations

• SecondOrder.Language.zf.omega = SecondOrder.Language.zf.Func.omega✝ ⬝ᶠ []ᵥ

def SecondOrder.Language.zf.termω : Lean.ParserDescr

Equations

• SecondOrder.Language.zf.termω = Lean.ParserDescr.node `SecondOrder.Language.zf.termω 1024 (Lean.ParserDescr.symbol "ω")

def SecondOrder.Language.zf.mem {l : List Ty} (t₁ t₂ : zf.Term l) : zf.Formula l

Equations

• SecondOrder.Language.zf.mem t₁ t₂ = SecondOrder.Language.zf.Rel.mem✝ ⬝ʳ [t₁, t₂]ᵥ

def SecondOrder.Language.zf.«term_∈'_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def SecondOrder.Language.zf.globalChoice : zf.Sentence

Equations

• SecondOrder.Language.zf.globalChoice = ∃ᶠ[1]∀' (∃' SecondOrder.Language.zf.mem #0 #1 ⇒ SecondOrder.Language.zf.mem (1 ⬝ᶠᵛ [#0]ᵥ) #0)

def SecondOrder.Language.zf.V (κ : InaccessibleCardinal) : Type (u + 1)

Equations

• SecondOrder.Language.zf.V κ = ↑(ZFSet.vonNeumann (↑κ).ord).toSet

@[simp]

theorem SecondOrder.Language.zf.V.val_inj {κ : InaccessibleCardinal} {x y : V κ} : x = y ↔ ↑x = ↑y

instance SecondOrder.Language.zf.V.instHasStructure {κ : InaccessibleCardinal} : zf.HasStructure (V κ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SecondOrder.Language.zf.V.interp_empty {l : List Ty} {κ : InaccessibleCardinal} {ρ : Assignment (V κ) l} : ↑(⟦ ∅ ⟧ₜ V κ, ρ) = ∅

@[simp]

theorem SecondOrder.Language.zf.V.interp_insert {l : List Ty} {κ : InaccessibleCardinal} {t₁ t₂ : zf.Term l} {ρ : Assignment (V κ) l} : ↑(⟦ insert t₁ t₂ ⟧ₜ V κ, ρ) = insert ↑(⟦ t₁ ⟧ₜ V κ, ρ) ↑(⟦ t₂ ⟧ₜ V κ, ρ)

@[simp]

theorem SecondOrder.Language.zf.V.interp_sUnion {l : List Ty} {κ : InaccessibleCardinal} {t : zf.Term l} {ρ : Assignment (V κ) l} : ↑(⟦ sUnion t ⟧ₜ V κ, ρ) = (↑(⟦ t ⟧ₜ V κ, ρ)).sUnion

@[simp]

theorem SecondOrder.Language.zf.V.interp_powerset {l : List Ty} {κ : InaccessibleCardinal} {t : zf.Term l} {ρ : Assignment (V κ) l} : ↑(⟦ powerset t ⟧ₜ V κ, ρ) = (↑(⟦ t ⟧ₜ V κ, ρ)).powerset

@[simp]

theorem SecondOrder.Language.zf.V.interp_omega {l : List Ty} {κ : InaccessibleCardinal} {ρ : Assignment (V κ) l} : ↑(⟦ omega ⟧ₜ V κ, ρ) = ZFSet.omega

@[simp]

theorem SecondOrder.Language.zf.V.satisfy_mem {l : List Ty} {κ : InaccessibleCardinal} {t₁ t₂ : zf.Term l} {ρ : Assignment (V κ) l} : V κ ⊨[ρ] mem t₁ t₂ ↔ ↑(⟦ t₁ ⟧ₜ V κ, ρ) ∈ ↑(⟦ t₂ ⟧ₜ V κ, ρ)

inductive SecondOrder.Language.Theory.ZF₂ : zf.Theory

• ax_ext : ZF₂ (∀' ∀' (∀' (zf.mem #0 #2 ⇔ zf.mem #0 #1) ⇒ #1 ≐ #0))
• ax_empty : ZF₂ (∀' (~ zf.mem #0 ∅))
• ax_insert : ZF₂ (∀' ∀' ∀' (zf.mem (#0) (insert #2 #1) ⇔ zf.mem #0 #1 ⩒ #0 ≐ #2))
• ax_union : ZF₂ (∀' ∀' (zf.mem (#0) (zf.sUnion #1) ⇔ ∃' (zf.mem #0 #2 ⩑ zf.mem #1 #0)))
• ax_powerset : ZF₂ (∀' ∀' (zf.mem (#0) (zf.powerset #1) ⇔ ∀' (zf.mem #0 #1 ⇒ zf.mem #0 #2)))
• ax_replacement : ZF₂ (∀' ∀ᶠ[1]∃' ∀' (zf.mem #0 #1 ⇔ ∃' (zf.mem #0 #4 ⩑ #1 ≐ 3 ⬝ᶠᵛ [#0]ᵥ)))
• ax_infinity : ZF₂ (zf.mem ∅ zf.omega ⩑ ∀' (zf.mem (#0) zf.omega ⇒ zf.mem (insert #0 #0) zf.omega) ⩑ ∀' (zf.mem ∅ #0 ⩑ ∀' (zf.mem #0 #1 ⇒ zf.mem (insert #0 #0) #1) ⇒ ∀' (zf.mem (#0) zf.omega ⇒ zf.mem #0 #1)))
• ax_regularity : ZF₂ (∀' (∃' zf.mem #0 #1 ⇒ ∃' (zf.mem #0 #1 ⩑ ~ ∃' (zf.mem #0 #2 ⩑ zf.mem #0 #1))))

instance SecondOrder.Language.Theory.ZF₂.instIsModelV {κ : InaccessibleCardinal} : ZF₂.IsModel (zf.V κ)

instance SecondOrder.Language.Theory.ZF₂.instMembershipDom {M : ZF₂.Model} : Membership M.Dom M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.instMembershipDom = { mem := fun (y x : M.Dom) => M.interpRel SecondOrder.Language.zf.Rel.mem✝ [x, y]ᵥ }

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.satisfy_mem {l : List Ty} {M : ZF₂.Model} {t₁ t₂ : zf.Term l} {ρ : Assignment M.Dom l} : M.Dom ⊨[ρ] zf.mem t₁ t₂ ↔ ⟦ t₁ ⟧ₜ M.Dom, ρ ∈ ⟦ t₂ ⟧ₜ M.Dom, ρ

theorem SecondOrder.Language.Theory.ZF₂.ext {M : ZF₂.Model} {x y : M.Dom} : (∀ (z : M.Dom), z ∈ x ↔ z ∈ y) → x = y

theorem SecondOrder.Language.Theory.ZF₂.ext_iff {M : ZF₂.Model} {x y : M.Dom} : x = y ↔ ∀ (z : M.Dom), z ∈ x ↔ z ∈ y

instance SecondOrder.Language.Theory.ZF₂.instEmptyCollectionDom {M : ZF₂.Model} : EmptyCollection M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.instEmptyCollectionDom = { emptyCollection := M.interpFunc SecondOrder.Language.zf.Func.empty✝ []ᵥ }

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.interp_empty {l : List Ty} {M : ZF₂.Model} {ρ : Assignment M.Dom l} : ⟦ ∅ ⟧ₜ M.Dom, ρ = ∅

instance SecondOrder.Language.Theory.ZF₂.instInhabitedDom {M : ZF₂.Model} : Inhabited M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.instInhabitedDom = { default := ∅ }

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.mem_empty {M : ZF₂.Model} {x : M.Dom} : x ∉ ∅

def SecondOrder.Language.Theory.ZF₂.Nonempty {M : ZF₂.Model} (x : M.Dom) : Prop

Equations

• SecondOrder.Language.Theory.ZF₂.Nonempty x = ∃ (y : M.Dom), y ∈ x

theorem SecondOrder.Language.Theory.ZF₂.nonempty_iff {M : ZF₂.Model} {x : M.Dom} : Nonempty x ↔ x ≠ ∅

instance SecondOrder.Language.Theory.ZF₂.instInsertDom {M : ZF₂.Model} : Insert M.Dom M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.instInsertDom = { insert := fun (x1 x2 : M.Dom) => M.interpFunc SecondOrder.Language.zf.Func.insert✝ [x1, x2]ᵥ }

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.interp_insert {l : List Ty} {M : ZF₂.Model} {t₁ t₂ : zf.Term l} {ρ : Assignment M.Dom l} : ⟦ insert t₁ t₂ ⟧ₜ M.Dom, ρ = insert (⟦ t₁ ⟧ₜ M.Dom, ρ) (⟦ t₂ ⟧ₜ M.Dom, ρ)

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.mem_insert {M : ZF₂.Model} {x y z : M.Dom} : z ∈ insert x y ↔ z ∈ y ∨ z = x

instance SecondOrder.Language.Theory.ZF₂.instSingletonDom {M : ZF₂.Model} : Singleton M.Dom M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.instSingletonDom = { singleton := fun (x : M.Dom) => insert x ∅ }

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.mem_singleton {M : ZF₂.Model} {x y : M.Dom} : y ∈ {x} ↔ y = x

def SecondOrder.Language.Theory.ZF₂.sUnion {M : ZF₂.Model} (x : M.Dom) : M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.sUnion x = M.interpFunc SecondOrder.Language.zf.Func.sUnion✝ [x]ᵥ

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.interp_sUnion {l : List Ty} {M : ZF₂.Model} {t : zf.Term l} {ρ : Assignment M.Dom l} : ⟦ zf.sUnion t ⟧ₜ M.Dom, ρ = sUnion (⟦ t ⟧ₜ M.Dom, ρ)

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.mem_sUnion {M : ZF₂.Model} {x y : M.Dom} : y ∈ sUnion x ↔ ∃ z ∈ x, y ∈ z

instance SecondOrder.Language.Theory.ZF₂.instHasSubsetDom {M : ZF₂.Model} : HasSubset M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.instHasSubsetDom = { Subset := fun (x1 x2 : M.Dom) => ∀ ⦃z : M.Dom⦄, z ∈ x1 → z ∈ x2 }

theorem SecondOrder.Language.Theory.ZF₂.subset_iff {M : ZF₂.Model} {x y : M.Dom} : x ⊆ y ↔ ∀ z ∈ x, z ∈ y

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.subset_refl {M : ZF₂.Model} {x : M.Dom} : x ⊆ x

theorem SecondOrder.Language.Theory.ZF₂.subset_antisymm {M : ZF₂.Model} {x y : M.Dom} : x ⊆ y → y ⊆ x → x = y

theorem SecondOrder.Language.Theory.ZF₂.subset_trans {M : ZF₂.Model} {x y z : M.Dom} : x ⊆ y → y ⊆ z → x ⊆ z

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.empty_subset {M : ZF₂.Model} {x : M.Dom} : ∅ ⊆ x

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.subset_insert {M : ZF₂.Model} {x y : M.Dom} : x ⊆ insert y x

instance SecondOrder.Language.Theory.ZF₂.instHasSSubsetDom {M : ZF₂.Model} : HasSSubset M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.instHasSSubsetDom = { SSubset := fun (x y : M.Dom) => x ⊆ y ∧ x ≠ y }

theorem SecondOrder.Language.Theory.ZF₂.ssubset_iff {M : ZF₂.Model} {x y : M.Dom} : x ⊂ y ↔ x ⊆ y ∧ x ≠ y

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.ssubset_irrefl {M : ZF₂.Model} {x : M.Dom} : ¬x ⊂ x

theorem SecondOrder.Language.Theory.ZF₂.ssubset_trans {M : ZF₂.Model} {x y z : M.Dom} : x ⊂ y → y ⊂ z → x ⊂ z

def SecondOrder.Language.Theory.ZF₂.powerset {M : ZF₂.Model} (x : M.Dom) : M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.powerset x = M.interpFunc SecondOrder.Language.zf.Func.powerset✝ [x]ᵥ

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.interp_powerset {l : List Ty} {M : ZF₂.Model} {t : zf.Term l} {ρ : Assignment M.Dom l} : ⟦ zf.powerset t ⟧ₜ M.Dom, ρ = powerset (⟦ t ⟧ₜ M.Dom, ρ)

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.mem_power {M : ZF₂.Model} {x y : M.Dom} : y ∈ powerset x ↔ y ⊆ x

theorem SecondOrder.Language.Theory.ZF₂.exists_replace {M : ZF₂.Model} (x : M.Dom) (f : M.Dom → M.Dom) : ∃ (y : M.Dom), ∀ (z : M.Dom), z ∈ y ↔ ∃ z' ∈ x, z = f z'

noncomputable def SecondOrder.Language.Theory.ZF₂.replace {M : ZF₂.Model} (x : M.Dom) (f : M.Dom → M.Dom) : M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.replace x f = Classical.choose ⋯

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.mem_replace {M : ZF₂.Model} {x y : M.Dom} {f : M.Dom → M.Dom} : y ∈ replace x f ↔ ∃ z ∈ x, y = f z

noncomputable def SecondOrder.Language.Theory.ZF₂.sep {M : ZF₂.Model} (x : M.Dom) (p : M.Dom → Prop) : M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.sep x p = SecondOrder.Language.Theory.ZF₂.sUnion (SecondOrder.Language.Theory.ZF₂.replace x fun (y : M.Dom) => if p y then {y} else ∅)

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.mem_sep {M : ZF₂.Model} {x y : M.Dom} {p : M.Dom → Prop} : x ∈ sep y p ↔ x ∈ y ∧ p x

noncomputable instance SecondOrder.Language.Theory.ZF₂.instInterDom {M : ZF₂.Model} : Inter M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.instInterDom = { inter := fun (x y : M.Dom) => SecondOrder.Language.Theory.ZF₂.sep x fun (x : M.Dom) => x ∈ y }

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.mem_intersect {M : ZF₂.Model} {x y z : M.Dom} : z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y

def SecondOrder.Language.Theory.ZF₂.omega (M : ZF₂.Model) : M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.omega M = M.interpFunc SecondOrder.Language.zf.Func.omega✝ []ᵥ

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.interp_omega {l : List Ty} {M : ZF₂.Model} {ρ : Assignment M.Dom l} : ⟦ zf.omega ⟧ₜ M.Dom, ρ = omega M

theorem SecondOrder.Language.Theory.ZF₂.empty_mem_omega {M : ZF₂.Model} : ∅ ∈ omega M

theorem SecondOrder.Language.Theory.ZF₂.succ_mem_omega {M : ZF₂.Model} {x : M.Dom} : x ∈ omega M → insert x x ∈ omega M

theorem SecondOrder.Language.Theory.ZF₂.omega_minimal {M : ZF₂.Model} {x : M.Dom} : ∅ ∈ x → (∀ y ∈ x, insert y y ∈ x) → omega M ⊆ x

def SecondOrder.Language.Theory.ZF₂.ofNat {M : ZF₂.Model} : ℕ → M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.ofNat 0 = ∅
• SecondOrder.Language.Theory.ZF₂.ofNat n.succ = insert (SecondOrder.Language.Theory.ZF₂.ofNat n) (SecondOrder.Language.Theory.ZF₂.ofNat n)

theorem SecondOrder.Language.Theory.ZF₂.mem_omega_iff {M : ZF₂.Model} {x : M.Dom} : x ∈ omega M ↔ ∃ (n : ℕ), x = ofNat n

theorem SecondOrder.Language.Theory.ZF₂.regularity {M : ZF₂.Model} (x : M.Dom) : Nonempty x → ∃ y ∈ x, ¬Nonempty (x ∩ y)

theorem SecondOrder.Language.Theory.ZF₂.not_mem_self {M : ZF₂.Model} {x : M.Dom} : x ∉ x

theorem SecondOrder.Language.Theory.ZF₂.ssubset_succ {M : ZF₂.Model} {x : M.Dom} : x ⊂ insert x x

theorem SecondOrder.Language.Theory.ZF₂.ofNat_ssubset {M : ZF₂.Model} {n m : ℕ} : n < m → ofNat n ⊂ ofNat m

theorem SecondOrder.Language.Theory.ZF₂.ofNat_injective {M : ZF₂.Model} : Function.Injective ofNat

noncomputable def SecondOrder.Language.Theory.ZF₂.iUnionOmega {M : ZF₂.Model} (f : ℕ → M.Dom) : M.Dom

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.mem_iUnionOmega {M : ZF₂.Model} {x : M.Dom} {f : ℕ → M.Dom} : x ∈ iUnionOmega f ↔ ∃ (n : ℕ), x ∈ f n

def SecondOrder.Language.Theory.ZF₂.IsTransitive {M : ZF₂.Model} (x : M.Dom) : Prop

Equations

• SecondOrder.Language.Theory.ZF₂.IsTransitive x = ∀ y ∈ x, y ⊆ x

def SecondOrder.Language.Theory.ZF₂.trclIter {M : ZF₂.Model} (x : M.Dom) : ℕ → M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.trclIter x 0 = x
• SecondOrder.Language.Theory.ZF₂.trclIter x n.succ = SecondOrder.Language.Theory.ZF₂.sUnion (SecondOrder.Language.Theory.ZF₂.trclIter x n)

noncomputable def SecondOrder.Language.Theory.ZF₂.trcl {M : ZF₂.Model} (x : M.Dom) : M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.trcl x = SecondOrder.Language.Theory.ZF₂.iUnionOmega (SecondOrder.Language.Theory.ZF₂.trclIter x)

theorem SecondOrder.Language.Theory.ZF₂.trcl.self_subset {M : ZF₂.Model} {x : M.Dom} : x ⊆ trcl x

theorem SecondOrder.Language.Theory.ZF₂.trcl.transitive {M : ZF₂.Model} {x : M.Dom} : IsTransitive (trcl x)

theorem SecondOrder.Language.Theory.ZF₂.trcl.minimal {M : ZF₂.Model} {x : M.Dom} (y : M.Dom) : y ⊇ x → IsTransitive y → trcl x ⊆ y

theorem SecondOrder.Language.Theory.ZF₂.mem_wf {M : ZF₂.Model} : WellFounded fun (x1 x2 : M.Dom) => x1 ∈ x2

instance SecondOrder.Language.Theory.ZF₂.instIsWellFoundedDomMem {M : ZF₂.Model} : IsWellFounded M.Dom fun (x1 x2 : M.Dom) => x1 ∈ x2

instance SecondOrder.Language.Theory.ZF₂.instWellFoundedRelationDom {M : ZF₂.Model} : WellFoundedRelation M.Dom

Equations

• SecondOrder.Language.Theory.ZF₂.instWellFoundedRelationDom = { rel := fun (x1 x2 : M.Dom) => x1 ∈ x2, wf := ⋯ }

theorem SecondOrder.Language.Theory.ZF₂.satisfy_global_choice {M : ZF₂.Model} : M.Dom ⊨ₛ zf.globalChoice

Since GC (global choice) is true in the metalanguage (Lean), it is also true in any model of second-order ZF. In other words, GC (which implies AC) is no longer "independent" in second-order ZF.

def SecondOrder.Language.Theory.ZF₂.card {M : ZF₂.Model} (x : M.Dom) : Cardinal.{u}

Equations

• SecondOrder.Language.Theory.ZF₂.card x = Cardinal.mk ↑{y : M.Dom | y ∈ x}

theorem SecondOrder.Language.Theory.ZF₂.card_mono {M : ZF₂.Model} {x y : M.Dom} : x ⊆ y → card x ≤ card y

theorem SecondOrder.Language.Theory.ZF₂.card_powerset {M : ZF₂.Model} {x : M.Dom} : card (powerset x) = 2 ^ card x

theorem SecondOrder.Language.Theory.ZF₂.card_omega {M : ZF₂.Model} : card (omega M) = Cardinal.aleph0

theorem SecondOrder.Language.Theory.ZF₂.card_iUnion_ge_iSup {M : ZF₂.Model} {x : M.Dom} {f : M.Dom → M.Dom} : card (sUnion (replace x f)) ≥ ⨆ (y : { y : M.Dom // y ∈ x }), card (f ↑y)

noncomputable def SecondOrder.Language.Theory.ZF₂.kappa (M : ZF₂.Model) : Cardinal.{u}

Equations

• SecondOrder.Language.Theory.ZF₂.kappa M = iSup SecondOrder.Language.Theory.ZF₂.card

theorem SecondOrder.Language.Theory.ZF₂.card_lt_kappa {M : ZF₂.Model} {x : M.Dom} : card x < kappa M

theorem SecondOrder.Language.Theory.ZF₂.exists_of_card_lt_kappa {M : ZF₂.Model} {c : Cardinal.{u}} : c < kappa M → ∃ (x : M.Dom), c = card x

theorem SecondOrder.Language.Theory.ZF₂.kappa_gt_aleph0 {M : ZF₂.Model} : Cardinal.aleph0 < kappa M

theorem SecondOrder.Language.Theory.ZF₂.kappa_strong_limit {M : ZF₂.Model} : (kappa M).IsStrongLimit

theorem SecondOrder.Language.Theory.ZF₂.kappa_regular {M : ZF₂.Model} : (kappa M).IsRegular

theorem SecondOrder.Language.Theory.ZF₂.kappa_inaccessible {M : ZF₂.Model} : (kappa M).IsInaccessible

noncomputable def SecondOrder.Language.Theory.ZF₂.rank {M : ZF₂.Model} : M.Dom → Ordinal.{u}

Equations

• SecondOrder.Language.Theory.ZF₂.rank = IsWellFounded.rank fun (x1 x2 : M.Dom) => x1 ∈ x2

theorem SecondOrder.Language.Theory.ZF₂.rank_lt_kappa {M : ZF₂.Model} {x : M.Dom} : rank x < (kappa M).ord

@[irreducible]

noncomputable def SecondOrder.Language.Theory.ZF₂.toZFSet {M : ZF₂.Model} (x : M.Dom) : ZFSet.{u}

Equations

• SecondOrder.Language.Theory.ZF₂.toZFSet x = ZFSet.range fun (x_1 : { y : M.Dom // y ∈ x }) => match x_1 with | ⟨y, property⟩ => SecondOrder.Language.Theory.ZF₂.toZFSet y

theorem SecondOrder.Language.Theory.ZF₂.mem_toZFSet {M : ZF₂.Model} {x : M.Dom} {y : ZFSet.{u}} : y ∈ toZFSet x ↔ ∃ z ∈ x, y = toZFSet z

theorem SecondOrder.Language.Theory.ZF₂.toZFSet_injective {M : ZF₂.Model} : Function.Injective toZFSet

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.toZFSet_mem {M : ZF₂.Model} {x y : M.Dom} : toZFSet x ∈ toZFSet y ↔ x ∈ y

@[simp]

theorem SecondOrder.Language.Theory.ZF₂.toZFSet_subset {M : ZF₂.Model} {x y : M.Dom} : toZFSet x ⊆ toZFSet y ↔ x ⊆ y

theorem SecondOrder.Language.Theory.ZF₂.toZFSet_empty {M : ZF₂.Model} : toZFSet ∅ = ∅

theorem SecondOrder.Language.Theory.ZF₂.toZFSet_insert {M : ZF₂.Model} {x y : M.Dom} : toZFSet (insert x y) = insert (toZFSet x) (toZFSet y)

theorem SecondOrder.Language.Theory.ZF₂.toZFSet_union {M : ZF₂.Model} {x : M.Dom} : toZFSet (sUnion x) = (toZFSet x).sUnion

theorem SecondOrder.Language.Theory.ZF₂.toZFSet_powerset {M : ZF₂.Model} {x : M.Dom} : toZFSet (powerset x) = (toZFSet x).powerset

theorem SecondOrder.Language.Theory.ZF₂.toZFSet_nat {M : ZF₂.Model} {n : ℕ} : toZFSet (ofNat n) = ZFSet.ofNat n

theorem SecondOrder.Language.Theory.ZF₂.toZFSet_omega {M : ZF₂.Model} : toZFSet (omega M) = ZFSet.omega

theorem SecondOrder.Language.Theory.ZF₂.rank_toZFSet {M : ZF₂.Model} {x : M.Dom} : (toZFSet x).rank = rank x

theorem SecondOrder.Language.Theory.ZF₂.toZFSet_surjective_V_kappa {M : ZF₂.Model} {x : ZFSet.{u}} : x ∈ ZFSet.vonNeumann (kappa M).ord → ∃ (y : M.Dom), toZFSet y = x

theorem SecondOrder.Language.Theory.ZF₂.iso_V (M : ZF₂.Model) : ∃ (κ : InaccessibleCardinal), _root_.Nonempty (M.toStructure ≃ᴹ Structure.of (zf.V κ))