Metamath Proof Explorer

Theorem omelaxinf2

Description: A transitive class that contains _om models the Axiom of Infinity ax-inf2 . Lemma II.2.11(7) of Kunen2 p. 114. Kunen has the additional hypotheses that the Extensionality, Separation, Pairing, and Union axioms are true in M . This, apparently, is because Kunen's statement of the Axiom of Infinity uses the defined notions (/) and suc , and these axioms guarantee that these notions are well-defined. When we state the axiom using primitives only, the need for these hypotheses disappears.

The antecedent of this theorem is not enough to guarantee that the class models the alternate axiom ax-inf . (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Assertion omelaxinf2 ⊢ Tr ⁡ M ∧ ω ∈ M → ∃ x ∈ M ∃ y ∈ M y ∈ x ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ x → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y

Proof

Step Hyp Ref Expression
1 trss ⊢ Tr ⁡ M → ω ∈ M → ω ⊆ M
2 1 imp ⊢ Tr ⁡ M ∧ ω ∈ M → ω ⊆ M
3 omssaxinf2 ⊢ ω ⊆ M ∧ ω ∈ M → ∃ x ∈ M ∃ y ∈ M y ∈ x ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ x → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
4 2 3 sylancom ⊢ Tr ⁡ M ∧ ω ∈ M → ∃ x ∈ M ∃ y ∈ M y ∈ x ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ x → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y