| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elnns 28344 | . . . 4
⊢ (𝑖 ∈ ℕs
↔ (𝑖 ∈
ℕ0s ∧ 𝑖 ≠ 0s )) | 
| 2 |  | df-ne 2940 | . . . . . . 7
⊢ (𝑖 ≠ 0s ↔ ¬
𝑖 = 0s
) | 
| 3 |  | n0s0suc 28346 | . . . . . . . 8
⊢ (𝑖 ∈ ℕ0s
→ (𝑖 = 0s
∨ ∃𝑗 ∈
ℕ0s 𝑖 =
(𝑗 +s
1s ))) | 
| 4 | 3 | ord 864 | . . . . . . 7
⊢ (𝑖 ∈ ℕ0s
→ (¬ 𝑖 =
0s → ∃𝑗 ∈ ℕ0s 𝑖 = (𝑗 +s 1s
))) | 
| 5 | 2, 4 | biimtrid 242 | . . . . . 6
⊢ (𝑖 ∈ ℕ0s
→ (𝑖 ≠
0s → ∃𝑗 ∈ ℕ0s 𝑖 = (𝑗 +s 1s
))) | 
| 6 | 5 | imp 406 | . . . . 5
⊢ ((𝑖 ∈ ℕ0s
∧ 𝑖 ≠ 0s
) → ∃𝑗 ∈
ℕ0s 𝑖 =
(𝑗 +s
1s )) | 
| 7 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑖 = 0s → (𝑖 +s 1s ) =
( 0s +s 1s )) | 
| 8 |  | 1sno 27873 | . . . . . . . . . . . . . 14
⊢ 
1s ∈  No | 
| 9 |  | addslid 28002 | . . . . . . . . . . . . . 14
⊢ (
1s ∈  No  → ( 0s
+s 1s ) = 1s ) | 
| 10 | 8, 9 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ (
0s +s 1s ) = 1s | 
| 11 | 7, 10 | eqtrdi 2792 | . . . . . . . . . . . 12
⊢ (𝑖 = 0s → (𝑖 +s 1s ) =
1s ) | 
| 12 | 11 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑖 = 0s →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = 1s )) | 
| 13 | 12 | rexbidv 3178 | . . . . . . . . . 10
⊢ (𝑖 = 0s →
(∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = 1s )) | 
| 14 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (𝑖 +s 1s ) = (𝑘 +s 1s
)) | 
| 15 | 14 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑘 +s 1s
))) | 
| 16 | 15 | rexbidv 3178 | . . . . . . . . . 10
⊢ (𝑖 = 𝑘 → (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑘 +s 1s
))) | 
| 17 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑖 = (𝑘 +s 1s ) → (𝑖 +s 1s ) =
((𝑘 +s
1s ) +s 1s )) | 
| 18 | 17 | eqeq2d 2747 | . . . . . . . . . . . 12
⊢ (𝑖 = (𝑘 +s 1s ) →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = ((𝑘 +s 1s ) +s
1s ))) | 
| 19 | 18 | rexbidv 3178 | . . . . . . . . . . 11
⊢ (𝑖 = (𝑘 +s 1s ) →
(∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = ((𝑘 +s 1s ) +s
1s ))) | 
| 20 |  | fveqeq2 6914 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = ((𝑘 +s 1s ) +s
1s ) ↔ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑧) = ((𝑘 +s 1s ) +s
1s ))) | 
| 21 | 20 | cbvrexvw 3237 | . . . . . . . . . . 11
⊢
(∃𝑦 ∈
ω ((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = ((𝑘 +s 1s ) +s
1s ) ↔ ∃𝑧 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑧) = ((𝑘 +s 1s ) +s
1s )) | 
| 22 | 19, 21 | bitrdi 287 | . . . . . . . . . 10
⊢ (𝑖 = (𝑘 +s 1s ) →
(∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
∃𝑧 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑧) = ((𝑘 +s 1s ) +s
1s ))) | 
| 23 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (𝑖 +s 1s ) = (𝑗 +s 1s
)) | 
| 24 | 23 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑗 +s 1s
))) | 
| 25 | 24 | rexbidv 3178 | . . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑗 +s 1s
))) | 
| 26 |  | peano1 7911 | . . . . . . . . . . 11
⊢ ∅
∈ ω | 
| 27 |  | 1nns 28353 | . . . . . . . . . . . 12
⊢ 
1s ∈ ℕs | 
| 28 |  | fr0g 8477 | . . . . . . . . . . . 12
⊢ (
1s ∈ ℕs → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘∅) = 1s
) | 
| 29 | 27, 28 | ax-mp 5 | . . . . . . . . . . 11
⊢
((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘∅) =
1s | 
| 30 |  | fveqeq2 6914 | . . . . . . . . . . . 12
⊢ (𝑦 = ∅ → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = 1s ↔ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘∅) = 1s
)) | 
| 31 | 30 | rspcev 3621 | . . . . . . . . . . 11
⊢ ((∅
∈ ω ∧ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘∅) = 1s ) →
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = 1s ) | 
| 32 | 26, 29, 31 | mp2an 692 | . . . . . . . . . 10
⊢
∃𝑦 ∈
ω ((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = 1s | 
| 33 |  | fveqeq2 6914 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 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 7913 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) | 
| 35 |  | ovex 7465 | . . . . . . . . . . . . . . 15
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) +s 1s ) ∈
V | 
| 36 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω) | 
| 37 |  | oveq1 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑥 → (𝑧 +s 1s ) = (𝑥 +s 1s
)) | 
| 38 |  | oveq1 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) → (𝑧 +s 1s ) =
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) +s 1s
)) | 
| 39 | 36, 37, 38 | frsucmpt2 8481 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ω ∧
(((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 691 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) +s 1s
)) | 
| 41 | 33, 34, 40 | rspcedvdw 3624 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ω →
∃𝑧 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑧) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) +s 1s
)) | 
| 42 | 41 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ0s
∧ 𝑦 ∈ ω)
→ ∃𝑧 ∈
ω ((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑧) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) +s 1s
)) | 
| 43 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑘 +s 1s ) →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) +s 1s ) = ((𝑘 +s 1s )
+s 1s )) | 
| 44 | 43 | eqeq2d 2747 | . . . . . . . . . . . . 13
⊢
(((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 3178 | . . . . . . . . . . . 12
⊢
(((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 245 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ0s
∧ 𝑦 ∈ ω)
→ (((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑘 +s 1s ) →
∃𝑧 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑧) = ((𝑘 +s 1s ) +s
1s ))) | 
| 47 | 46 | rexlimdva 3154 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ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 28338 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ0s
→ ∃𝑦 ∈
ω ((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑗 +s 1s
)) | 
| 49 |  | frfnom 8476 | . . . . . . . . . 10
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω) Fn ω | 
| 50 |  | fvelrnb 6968 | . . . . . . . . . 10
⊢
((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 5 | . . . . . . . . 9
⊢ ((𝑗 +s 1s )
∈ ran (rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω) ↔ ∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = (𝑗 +s 1s
)) | 
| 52 | 48, 51 | sylibr 234 | . . . . . . . 8
⊢ (𝑗 ∈ ℕ0s
→ (𝑗 +s
1s ) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)) | 
| 53 |  | df-ima 5697 | . . . . . . . 8
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω) | 
| 54 | 52, 53 | eleqtrrdi 2851 | . . . . . . 7
⊢ (𝑗 ∈ ℕ0s
→ (𝑗 +s
1s ) ∈ (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω)) | 
| 55 |  | eleq1 2828 | . . . . . . 7
⊢ (𝑖 = (𝑗 +s 1s ) → (𝑖 ∈ (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω) ↔ (𝑗 +s 1s ) ∈
(rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) “ ω))) | 
| 56 | 54, 55 | syl5ibrcom 247 | . . . . . 6
⊢ (𝑗 ∈ ℕ0s
→ (𝑖 = (𝑗 +s 1s )
→ 𝑖 ∈ (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω))) | 
| 57 | 56 | rexlimiv 3147 | . . . . 5
⊢
(∃𝑗 ∈
ℕ0s 𝑖 =
(𝑗 +s
1s ) → 𝑖
∈ (rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) “ ω)) | 
| 58 | 6, 57 | syl 17 | . . . 4
⊢ ((𝑖 ∈ ℕ0s
∧ 𝑖 ≠ 0s
) → 𝑖 ∈
(rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) “ ω)) | 
| 59 | 1, 58 | sylbi 217 | . . 3
⊢ (𝑖 ∈ ℕs
→ 𝑖 ∈ (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω)) | 
| 60 | 59 | ssriv 3986 | . 2
⊢
ℕs ⊆ (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω) | 
| 61 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑘 = ∅ → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘∅)) | 
| 62 | 61 | eleq1d 2825 | . . . . . 6
⊢ (𝑘 = ∅ → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) ∈ ℕs ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘∅) ∈
ℕs)) | 
| 63 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑘 = 𝑗 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑗)) | 
| 64 | 63 | eleq1d 2825 | . . . . . 6
⊢ (𝑘 = 𝑗 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) ∈ ℕs ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) ∈
ℕs)) | 
| 65 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑘 = suc 𝑗 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘suc 𝑗)) | 
| 66 | 65 | eleq1d 2825 | . . . . . 6
⊢ (𝑘 = suc 𝑗 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) ∈ ℕs ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘suc 𝑗) ∈
ℕs)) | 
| 67 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑘 = 𝑖 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑖)) | 
| 68 | 67 | eleq1d 2825 | . . . . . 6
⊢ (𝑘 = 𝑖 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) ∈ ℕs ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑖) ∈
ℕs)) | 
| 69 | 29, 27 | eqeltri 2836 | . . . . . 6
⊢
((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘∅) ∈
ℕs | 
| 70 |  | peano2nns 28354 | . . . . . . 7
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) ∈ ℕs →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) +s 1s ) ∈
ℕs) | 
| 71 |  | ovex 7465 | . . . . . . . . 9
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) +s 1s ) ∈
V | 
| 72 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑦 +s 1s ) = (𝑥 +s 1s
)) | 
| 73 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑦 = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑗) → (𝑦 +s 1s ) =
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) +s 1s
)) | 
| 74 | 36, 72, 73 | frsucmpt2 8481 | . . . . . . . . 9
⊢ ((𝑗 ∈ ω ∧
(((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 691 | . . . . . . . 8
⊢ (𝑗 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘suc 𝑗) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑗) +s 1s
)) | 
| 76 | 75 | eleq1d 2825 | . . . . . . 7
⊢ (𝑗 ∈ ω →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘suc 𝑗) ∈ ℕs ↔
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) +s 1s ) ∈
ℕs)) | 
| 77 | 70, 76 | imbitrrid 246 | . . . . . 6
⊢ (𝑗 ∈ ω →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) ∈ ℕs →
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘suc 𝑗) ∈
ℕs)) | 
| 78 | 62, 64, 66, 68, 69, 77 | finds 7919 | . . . . 5
⊢ (𝑖 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑖) ∈
ℕs) | 
| 79 | 78 | rgen 3062 | . . . 4
⊢
∀𝑖 ∈
ω ((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑖) ∈ ℕs | 
| 80 |  | fnfvrnss 7140 | . . . 4
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω) Fn ω ∧
∀𝑖 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑖) ∈ ℕs) → ran
(rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω) ⊆
ℕs) | 
| 81 | 49, 79, 80 | mp2an 692 | . . 3
⊢ ran
(rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω) ⊆
ℕs | 
| 82 | 53, 81 | eqsstri 4029 | . 2
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) “ ω) ⊆
ℕs | 
| 83 | 60, 82 | eqssi 3999 | 1
⊢
ℕs = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω) |