This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axinf

Description: The first version of the Axiom of Infinity ax-inf proved from the second version ax-inf2 . Note that we didn't use ax-reg , unlike the other direction axinf2 . (Contributed by NM, 24-Apr-2009)

Ref Expression
Assertion axinf ⊢ ∃ y x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y

Proof

Step Hyp Ref Expression
1 omex ⊢ ω ∈ V
2 inf0 ⊢ ω ∈ V → ∃ y x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y
3 1 2 ax-mp ⊢ ∃ y x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y