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 ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω )
2 rdgfun Fun rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 )
3 omex ω ∈ V
4 funimaexg ( ( Fun rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ∧ ω ∈ V ) → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω ) ∈ V )
5 2 3 4 mp2an ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω ) ∈ V
6 1 5 eqeltri ℕ ∈ V