| Step | Hyp | Ref
| Expression |
| 1 | | elnns 28491 |
. . . 4
⊢ (𝑖 ∈ ℕs
↔ (𝑖 ∈
ℕ0s ∧ 𝑖 ≠ 0s )) |
| 2 | | df-ne 2961 |
. . . . . . 7
⊢ (𝑖 ≠ 0s ↔ ¬
𝑖 = 0s
) |
| 3 | | n0s0suc 28493 |
. . . . . . . 8
⊢ (𝑖 ∈ ℕ0s
→ (𝑖 = 0s
∨ ∃𝑗 ∈
ℕ0s 𝑖 =
(𝑗 +s
1s ))) |
| 4 | 3 | ord 877 |
. . . . . . 7
⊢ (𝑖 ∈ ℕ0s
→ (¬ 𝑖 =
0s → ∃𝑗 ∈ ℕ0s 𝑖 = (𝑗 +s 1s
))) |
| 5 | 2, 4 | biimtrid 245 |
. . . . . 6
⊢ (𝑖 ∈ ℕ0s
→ (𝑖 ≠
0s → ∃𝑗 ∈ ℕ0s 𝑖 = (𝑗 +s 1s
))) |
| 6 | 5 | imp 411 |
. . . . 5
⊢ ((𝑖 ∈ ℕ0s
∧ 𝑖 ≠ 0s
) → ∃𝑗 ∈
ℕ0s 𝑖 =
(𝑗 +s
1s )) |
| 7 | | oveq1 7407 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 0s → (𝑖 +s 1s ) =
( 0s +s 1s )) |
| 8 | | 1no 27961 |
. . . . . . . . . . . . . 14
⊢
1s ∈ No |
| 9 | | addslid 28119 |
. . . . . . . . . . . . . 14
⊢ (
1s ∈ No → ( 0s
+s 1s ) = 1s ) |
| 10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (
0s +s 1s ) = 1s |
| 11 | 7, 10 | eqtrdi 2816 |
. . . . . . . . . . . 12
⊢ (𝑖 = 0s → (𝑖 +s 1s ) =
1s ) |
| 12 | 11 | eqeq2d 2776 |
. . . . . . . . . . 11
⊢ (𝑖 = 0s →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = 1s )) |
| 13 | 12 | rexbidv 3189 |
. . . . . . . . . 10
⊢ (𝑖 = 0s →
(∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = 1s )) |
| 14 | | oveq1 7407 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (𝑖 +s 1s ) = (𝑘 +s 1s
)) |
| 15 | 14 | eqeq2d 2776 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑘 +s 1s
))) |
| 16 | 15 | rexbidv 3189 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑘 +s 1s
))) |
| 17 | | oveq1 7407 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑘 +s 1s ) → (𝑖 +s 1s ) =
((𝑘 +s
1s ) +s 1s )) |
| 18 | 17 | eqeq2d 2776 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑘 +s 1s ) →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = ((𝑘 +s 1s ) +s
1s ))) |
| 19 | 18 | rexbidv 3189 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑘 +s 1s ) →
(∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = ((𝑘 +s 1s ) +s
1s ))) |
| 20 | | fveqeq2 6880 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = ((𝑘 +s 1s ) +s
1s ) ↔ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑧) = ((𝑘 +s 1s ) +s
1s ))) |
| 21 | 20 | cbvrexvw 3244 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
ω ((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = ((𝑘 +s 1s ) +s
1s ) ↔ ∃𝑧 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑧) = ((𝑘 +s 1s ) +s
1s )) |
| 22 | 19, 21 | bitrdi 290 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑘 +s 1s ) →
(∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
∃𝑧 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑧) = ((𝑘 +s 1s ) +s
1s ))) |
| 23 | | oveq1 7407 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (𝑖 +s 1s ) = (𝑗 +s 1s
)) |
| 24 | 23 | eqeq2d 2776 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑗 +s 1s
))) |
| 25 | 24 | rexbidv 3189 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = (𝑖 +s 1s ) ↔
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑗 +s 1s
))) |
| 26 | | peano1 7873 |
. . . . . . . . . . 11
⊢ ∅
∈ ω |
| 27 | | 1nns 28500 |
. . . . . . . . . . . 12
⊢
1s ∈ ℕs |
| 28 | | fr0g 8411 |
. . . . . . . . . . . 12
⊢ (
1s ∈ ℕs → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘∅) = 1s
) |
| 29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘∅) =
1s |
| 30 | | fveqeq2 6880 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∅ → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) = 1s ↔ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘∅) = 1s
)) |
| 31 | 30 | rspcev 3584 |
. . . . . . . . . . 11
⊢ ((∅
∈ ω ∧ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘∅) = 1s ) →
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = 1s ) |
| 32 | 26, 29, 31 | mp2an 704 |
. . . . . . . . . 10
⊢
∃𝑦 ∈
ω ((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = 1s |
| 33 | | fveqeq2 6880 |
. . . . . . . . . . . . . 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 7874 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) |
| 35 | | ovex 7433 |
. . . . . . . . . . . . . . 15
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) +s 1s ) ∈
V |
| 36 | | eqid 2765 |
. . . . . . . . . . . . . . . 16
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω) |
| 37 | | oveq1 7407 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑥 → (𝑧 +s 1s ) = (𝑥 +s 1s
)) |
| 38 | | oveq1 7407 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) → (𝑧 +s 1s ) =
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) +s 1s
)) |
| 39 | 36, 37, 38 | frsucmpt2 8415 |
. . . . . . . . . . . . . . 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 703 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) +s 1s
)) |
| 41 | 33, 34, 40 | rspcedvdw 3587 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ω →
∃𝑧 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑧) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) +s 1s
)) |
| 42 | 41 | adantl 486 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ0s
∧ 𝑦 ∈ ω)
→ ∃𝑧 ∈
ω ((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑧) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑦) +s 1s
)) |
| 43 | | oveq1 7407 |
. . . . . . . . . . . . . 14
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑘 +s 1s ) →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) +s 1s ) = ((𝑘 +s 1s )
+s 1s )) |
| 44 | 43 | eqeq2d 2776 |
. . . . . . . . . . . . 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 3189 |
. . . . . . . . . . . 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 248 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ0s
∧ 𝑦 ∈ ω)
→ (((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑘 +s 1s ) →
∃𝑧 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑧) = ((𝑘 +s 1s ) +s
1s ))) |
| 47 | 46 | rexlimdva 3166 |
. . . . . . . . . 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 28484 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ0s
→ ∃𝑦 ∈
ω ((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑦) = (𝑗 +s 1s
)) |
| 49 | | frfnom 8410 |
. . . . . . . . . 10
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω) Fn ω |
| 50 | | fvelrnb 6931 |
. . . . . . . . . 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 237 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0s
→ (𝑗 +s
1s ) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)) |
| 53 | | df-ima 5665 |
. . . . . . . 8
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω) |
| 54 | 52, 53 | eleqtrrdi 2876 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ0s
→ (𝑗 +s
1s ) ∈ (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω)) |
| 55 | | eleq1 2853 |
. . . . . . 7
⊢ (𝑖 = (𝑗 +s 1s ) → (𝑖 ∈ (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω) ↔ (𝑗 +s 1s ) ∈
(rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) “ ω))) |
| 56 | 54, 55 | syl5ibrcom 250 |
. . . . . 6
⊢ (𝑗 ∈ ℕ0s
→ (𝑖 = (𝑗 +s 1s )
→ 𝑖 ∈ (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω))) |
| 57 | 56 | rexlimiv 3159 |
. . . . 5
⊢
(∃𝑗 ∈
ℕ0s 𝑖 =
(𝑗 +s
1s ) → 𝑖
∈ (rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) “ ω)) |
| 58 | 6, 57 | syl 18 |
. . . 4
⊢ ((𝑖 ∈ ℕ0s
∧ 𝑖 ≠ 0s
) → 𝑖 ∈
(rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) “ ω)) |
| 59 | 1, 58 | sylbi 220 |
. . 3
⊢ (𝑖 ∈ ℕs
→ 𝑖 ∈ (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω)) |
| 60 | 59 | ssriv 3943 |
. 2
⊢
ℕs ⊆ (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω) |
| 61 | | fveq2 6871 |
. . . . . . 7
⊢ (𝑘 = ∅ → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘∅)) |
| 62 | 61 | eleq1d 2850 |
. . . . . 6
⊢ (𝑘 = ∅ → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) ∈ ℕs ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘∅) ∈
ℕs)) |
| 63 | | fveq2 6871 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑗)) |
| 64 | 63 | eleq1d 2850 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) ∈ ℕs ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) ∈
ℕs)) |
| 65 | | fveq2 6871 |
. . . . . . 7
⊢ (𝑘 = suc 𝑗 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘suc 𝑗)) |
| 66 | 65 | eleq1d 2850 |
. . . . . 6
⊢ (𝑘 = suc 𝑗 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) ∈ ℕs ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘suc 𝑗) ∈
ℕs)) |
| 67 | | fveq2 6871 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑖)) |
| 68 | 67 | eleq1d 2850 |
. . . . . 6
⊢ (𝑘 = 𝑖 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑘) ∈ ℕs ↔
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑖) ∈
ℕs)) |
| 69 | 29, 27 | eqeltri 2861 |
. . . . . 6
⊢
((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘∅) ∈
ℕs |
| 70 | | peano2nns 28501 |
. . . . . . 7
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) ∈ ℕs →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) +s 1s ) ∈
ℕs) |
| 71 | | ovex 7433 |
. . . . . . . . 9
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) +s 1s ) ∈
V |
| 72 | | oveq1 7407 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑦 +s 1s ) = (𝑥 +s 1s
)) |
| 73 | | oveq1 7407 |
. . . . . . . . . 10
⊢ (𝑦 = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑗) → (𝑦 +s 1s ) =
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) +s 1s
)) |
| 74 | 36, 72, 73 | frsucmpt2 8415 |
. . . . . . . . 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 703 |
. . . . . . . 8
⊢ (𝑗 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘suc 𝑗) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) ↾ ω)‘𝑗) +s 1s
)) |
| 76 | 75 | eleq1d 2850 |
. . . . . . 7
⊢ (𝑗 ∈ ω →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘suc 𝑗) ∈ ℕs ↔
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) +s 1s ) ∈
ℕs)) |
| 77 | 70, 76 | imbitrrid 249 |
. . . . . 6
⊢ (𝑗 ∈ ω →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑗) ∈ ℕs →
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘suc 𝑗) ∈
ℕs)) |
| 78 | 62, 64, 66, 68, 69, 77 | finds 7881 |
. . . . 5
⊢ (𝑖 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω)‘𝑖) ∈
ℕs) |
| 79 | 78 | rgen 3081 |
. . . 4
⊢
∀𝑖 ∈
ω ((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) ↾ ω)‘𝑖) ∈ ℕs |
| 80 | | fnfvrnss 7106 |
. . . 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 704 |
. . 3
⊢ ran
(rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 1s ) ↾ ω) ⊆
ℕs |
| 82 | 53, 81 | eqsstri 3985 |
. 2
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 1s ) “ ω) ⊆
ℕs |
| 83 | 60, 82 | eqssi 3955 |
1
⊢
ℕs = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω) |