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

Proof

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