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	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2		inf0	⊢ ( ω ∈ V → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )
3	1 2	ax-mp	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) )