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	$$⊢\exists y\left(x\in y\wedge \forall z\left(z\in y\to \exists w\left(z\in w\wedge w\in y\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
2		inf0	$$⊢\mathrm{\omega }\in \mathrm{V}\to \exists y\left(x\in y\wedge \forall z\left(z\in y\to \exists w\left(z\in w\wedge w\in y\right)\right)\right)$$
3	1 2	ax-mp	$$⊢\exists y\left(x\in y\wedge \forall z\left(z\in y\to \exists w\left(z\in w\wedge w\in y\right)\right)\right)$$