Theorem dfnns2

Description: Alternate definition of the positive surreal integers. Compare df-nn . (Contributed by Scott Fenton, 6-Aug-2025)

	Ref	Expression
Assertion	dfnns2	⊢ ℕs = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω )

Proof

Step	Hyp	Ref	Expression
1		elnns	⊢ ( 𝑖 ∈ ℕs ↔ ( 𝑖 ∈ ℕ0s ∧ 𝑖 ≠ 0s ) )
2		df-ne	⊢ ( 𝑖 ≠ 0s ↔ ¬ 𝑖 = 0s )
3		n0s0suc	⊢ ( 𝑖 ∈ ℕ0s → ( 𝑖 = 0s ∨ ∃ 𝑗 ∈ ℕ0s 𝑖 = ( 𝑗 +s 1s ) ) )
4	3	ord	⊢ ( 𝑖 ∈ ℕ0s → ( ¬ 𝑖 = 0s → ∃ 𝑗 ∈ ℕ0s 𝑖 = ( 𝑗 +s 1s ) ) )
5	2 4	biimtrid	⊢ ( 𝑖 ∈ ℕ0s → ( 𝑖 ≠ 0s → ∃ 𝑗 ∈ ℕ0s 𝑖 = ( 𝑗 +s 1s ) ) )
6	5	imp	⊢ ( ( 𝑖 ∈ ℕ0s ∧ 𝑖 ≠ 0s ) → ∃ 𝑗 ∈ ℕ0s 𝑖 = ( 𝑗 +s 1s ) )
7		oveq1	⊢ ( 𝑖 = 0s → ( 𝑖 +s 1s ) = ( 0s +s 1s ) )
8		1sno	⊢ 1s ∈ No
9		addslid	⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
10	8 9	ax-mp	⊢ ( 0s +s 1s ) = 1s
11	7 10	eqtrdi	⊢ ( 𝑖 = 0s → ( 𝑖 +s 1s ) = 1s )
12	11	eqeq2d	⊢ ( 𝑖 = 0s → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑖 +s 1s ) ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = 1s ) )
13	12	rexbidv	⊢ ( 𝑖 = 0s → ( ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑖 +s 1s ) ↔ ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = 1s ) )
14		oveq1	⊢ ( 𝑖 = 𝑘 → ( 𝑖 +s 1s ) = ( 𝑘 +s 1s ) )
15	14	eqeq2d	⊢ ( 𝑖 = 𝑘 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑖 +s 1s ) ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑘 +s 1s ) ) )
16	15	rexbidv	⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑖 +s 1s ) ↔ ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑘 +s 1s ) ) )
17		oveq1	⊢ ( 𝑖 = ( 𝑘 +s 1s ) → ( 𝑖 +s 1s ) = ( ( 𝑘 +s 1s ) +s 1s ) )
18	17	eqeq2d	⊢ ( 𝑖 = ( 𝑘 +s 1s ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑖 +s 1s ) ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( ( 𝑘 +s 1s ) +s 1s ) ) )
19	18	rexbidv	⊢ ( 𝑖 = ( 𝑘 +s 1s ) → ( ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑖 +s 1s ) ↔ ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( ( 𝑘 +s 1s ) +s 1s ) ) )
20		fveqeq2	⊢ ( 𝑦 = 𝑧 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( ( 𝑘 +s 1s ) +s 1s ) ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( 𝑘 +s 1s ) +s 1s ) ) )
21	20	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( ( 𝑘 +s 1s ) +s 1s ) ↔ ∃ 𝑧 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( 𝑘 +s 1s ) +s 1s ) )
22	19 21	bitrdi	⊢ ( 𝑖 = ( 𝑘 +s 1s ) → ( ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑖 +s 1s ) ↔ ∃ 𝑧 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( 𝑘 +s 1s ) +s 1s ) ) )
23		oveq1	⊢ ( 𝑖 = 𝑗 → ( 𝑖 +s 1s ) = ( 𝑗 +s 1s ) )
24	23	eqeq2d	⊢ ( 𝑖 = 𝑗 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑖 +s 1s ) ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑗 +s 1s ) ) )
25	24	rexbidv	⊢ ( 𝑖 = 𝑗 → ( ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑖 +s 1s ) ↔ ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑗 +s 1s ) ) )
26		peano1	⊢ ∅ ∈ ω
27		1nns	⊢ 1s ∈ ℕs
28		fr0g	⊢ ( 1s ∈ ℕs → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ ∅ ) = 1s )
29	27 28	ax-mp	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ ∅ ) = 1s
30		fveqeq2	⊢ ( 𝑦 = ∅ → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = 1s ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ ∅ ) = 1s ) )
31	30	rspcev	⊢ ( ( ∅ ∈ ω ∧ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ ∅ ) = 1s ) → ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = 1s )
32	26 29 31	mp2an	⊢ ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = 1s
33		fveqeq2	⊢ ( 𝑧 = suc 𝑦 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ suc 𝑦 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) ) )
34		peano2	⊢ ( 𝑦 ∈ ω → suc 𝑦 ∈ ω )
35		ovex	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) ∈ V
36		eqid	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω )
37		oveq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) )
38		oveq1	⊢ ( 𝑧 = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) → ( 𝑧 +s 1s ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) )
39	36 37 38	frsucmpt2	⊢ ( ( 𝑦 ∈ ω ∧ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) ∈ V ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ suc 𝑦 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) )
40	35 39	mpan2	⊢ ( 𝑦 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ suc 𝑦 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) )
41	33 34 40	rspcedvdw	⊢ ( 𝑦 ∈ ω → ∃ 𝑧 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) )
42	41	adantl	⊢ ( ( 𝑘 ∈ ℕ0s ∧ 𝑦 ∈ ω ) → ∃ 𝑧 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) )
43		oveq1	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑘 +s 1s ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) = ( ( 𝑘 +s 1s ) +s 1s ) )
44	43	eqeq2d	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑘 +s 1s ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( 𝑘 +s 1s ) +s 1s ) ) )
45	44	rexbidv	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑘 +s 1s ) → ( ∃ 𝑧 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) +s 1s ) ↔ ∃ 𝑧 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( 𝑘 +s 1s ) +s 1s ) ) )
46	42 45	syl5ibcom	⊢ ( ( 𝑘 ∈ ℕ0s ∧ 𝑦 ∈ ω ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑘 +s 1s ) → ∃ 𝑧 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( 𝑘 +s 1s ) +s 1s ) ) )
47	46	rexlimdva	⊢ ( 𝑘 ∈ ℕ0s → ( ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑘 +s 1s ) → ∃ 𝑧 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑧 ) = ( ( 𝑘 +s 1s ) +s 1s ) ) )
48	13 16 22 25 32 47	n0sind	⊢ ( 𝑗 ∈ ℕ0s → ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑗 +s 1s ) )
49		frfnom	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) Fn ω
50		fvelrnb	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) Fn ω → ( ( 𝑗 +s 1s ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ↔ ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑗 +s 1s ) ) )
51	49 50	ax-mp	⊢ ( ( 𝑗 +s 1s ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ↔ ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑦 ) = ( 𝑗 +s 1s ) )
52	48 51	sylibr	⊢ ( 𝑗 ∈ ℕ0s → ( 𝑗 +s 1s ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) )
53		df-ima	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω ) = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω )
54	52 53	eleqtrrdi	⊢ ( 𝑗 ∈ ℕ0s → ( 𝑗 +s 1s ) ∈ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω ) )
55		eleq1	⊢ ( 𝑖 = ( 𝑗 +s 1s ) → ( 𝑖 ∈ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω ) ↔ ( 𝑗 +s 1s ) ∈ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω ) ) )
56	54 55	syl5ibrcom	⊢ ( 𝑗 ∈ ℕ0s → ( 𝑖 = ( 𝑗 +s 1s ) → 𝑖 ∈ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω ) ) )
57	56	rexlimiv	⊢ ( ∃ 𝑗 ∈ ℕ0s 𝑖 = ( 𝑗 +s 1s ) → 𝑖 ∈ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω ) )
58	6 57	syl	⊢ ( ( 𝑖 ∈ ℕ0s ∧ 𝑖 ≠ 0s ) → 𝑖 ∈ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω ) )
59	1 58	sylbi	⊢ ( 𝑖 ∈ ℕs → 𝑖 ∈ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω ) )
60	59	ssriv	⊢ ℕs ⊆ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω )
61		fveq2	⊢ ( 𝑘 = ∅ → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑘 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ ∅ ) )
62	61	eleq1d	⊢ ( 𝑘 = ∅ → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑘 ) ∈ ℕs ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ ∅ ) ∈ ℕs ) )
63		fveq2	⊢ ( 𝑘 = 𝑗 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑘 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) )
64	63	eleq1d	⊢ ( 𝑘 = 𝑗 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑘 ) ∈ ℕs ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) ∈ ℕs ) )
65		fveq2	⊢ ( 𝑘 = suc 𝑗 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑘 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ suc 𝑗 ) )
66	65	eleq1d	⊢ ( 𝑘 = suc 𝑗 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑘 ) ∈ ℕs ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ suc 𝑗 ) ∈ ℕs ) )
67		fveq2	⊢ ( 𝑘 = 𝑖 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑘 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑖 ) )
68	67	eleq1d	⊢ ( 𝑘 = 𝑖 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑘 ) ∈ ℕs ↔ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑖 ) ∈ ℕs ) )
69	29 27	eqeltri	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ ∅ ) ∈ ℕs
70		peano2nns	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) ∈ ℕs → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) +s 1s ) ∈ ℕs )
71		ovex	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) +s 1s ) ∈ V
72		oveq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 +s 1s ) = ( 𝑥 +s 1s ) )
73		oveq1	⊢ ( 𝑦 = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) → ( 𝑦 +s 1s ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) +s 1s ) )
74	36 72 73	frsucmpt2	⊢ ( ( 𝑗 ∈ ω ∧ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) +s 1s ) ∈ V ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ suc 𝑗 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) +s 1s ) )
75	71 74	mpan2	⊢ ( 𝑗 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ suc 𝑗 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) +s 1s ) )
76	75	eleq1d	⊢ ( 𝑗 ∈ ω → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ suc 𝑗 ) ∈ ℕs ↔ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) +s 1s ) ∈ ℕs ) )
77	70 76	imbitrrid	⊢ ( 𝑗 ∈ ω → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑗 ) ∈ ℕs → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ suc 𝑗 ) ∈ ℕs ) )
78	62 64 66 68 69 77	finds	⊢ ( 𝑖 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑖 ) ∈ ℕs )
79	78	rgen	⊢ ∀ 𝑖 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑖 ) ∈ ℕs
80		fnfvrnss	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) Fn ω ∧ ∀ 𝑖 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ‘ 𝑖 ) ∈ ℕs ) → ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ⊆ ℕs )
81	49 79 80	mp2an	⊢ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) ↾ ω ) ⊆ ℕs
82	53 81	eqsstri	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω ) ⊆ ℕs
83	60 82	eqssi	⊢ ℕs = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω )