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 |
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 |