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 ⊢ ℕ ∈ V

Proof

Step Hyp Ref Expression
1 df-nn ⊢ ℕ = rec ⁡ x ∈ V ⟼ x + 1 1 ω
2 rdgfun ⊢ Fun ⁡ rec ⁡ x ∈ V ⟼ x + 1 1
3 omex ⊢ ω ∈ V
4 funimaexg ⊢ Fun ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ∧ ω ∈ V → rec ⁡ x ∈ V ⟼ x + 1 1 ω ∈ V
5 2 3 4 mp2an ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ω ∈ V
6 1 5 eqeltri ⊢ ℕ ∈ V