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	|- E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) )

Proof

Step	Hyp	Ref	Expression
1		omex	|- _om e. _V
2		inf0	|- ( _om e. _V -> E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) ) )
3	1 2	ax-mp	|- E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) )