Metamath Proof Explorer

Theorem nnexALT

Description: Alternate proof of nnex , more direct, that makes use of ax-rep . (Contributed by Mario Carneiro, 3-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	nnexALT	$⊢ ℕ \in V$

Proof

Step	Hyp	Ref	Expression
1		df-nn	$⊢ ℕ = rec ((x \in V ⟼ x + 1), 1) [ω]$
2		rdgfun	$⊢ Fun rec ((x \in V ⟼ x + 1), 1)$
3		omex	$⊢ ω \in V$
4		funimaexg	$⊢ (Fun rec ((x \in V ⟼ x + 1), 1) \land ω \in V) \to rec ((x \in V ⟼ x + 1), 1) [ω] \in V$
5	2 3 4	mp2an	$⊢ rec ((x \in V ⟼ x + 1), 1) [ω] \in V$
6	1 5	eqeltri	$⊢ ℕ \in V$