Step | Hyp | Ref
| Expression |
1 | | peano2 7086 |
. . . . 5
⊢ (𝐵 ∈ ω → suc 𝐵 ∈
ω) |
2 | | nnon 7071 |
. . . . 5
⊢ (suc
𝐵 ∈ ω → suc
𝐵 ∈
On) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐵 ∈ ω → suc 𝐵 ∈ On) |
4 | | omv 7592 |
. . . 4
⊢ ((𝐴 ∈ On ∧ suc 𝐵 ∈ On) → (𝐴 ·𝑜
suc 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅)‘suc 𝐵)) |
5 | 3, 4 | sylan2 491 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜
suc 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅)‘suc 𝐵)) |
6 | 1 | adantl 482 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → suc
𝐵 ∈
ω) |
7 | | fvres 6207 |
. . . 4
⊢ (suc
𝐵 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +𝑜
𝐴)), ∅) ↾
ω)‘suc 𝐵) =
(rec((𝑥 ∈ V ↦
(𝑥 +𝑜
𝐴)), ∅)‘suc
𝐵)) |
8 | 6, 7 | syl 17 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) →
((rec((𝑥 ∈ V ↦
(𝑥 +𝑜
𝐴)), ∅) ↾
ω)‘suc 𝐵) =
(rec((𝑥 ∈ V ↦
(𝑥 +𝑜
𝐴)), ∅)‘suc
𝐵)) |
9 | 5, 8 | eqtr4d 2659 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜
suc 𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅) ↾
ω)‘suc 𝐵)) |
10 | | ovex 6678 |
. . . . 5
⊢ (𝐴 ·𝑜
𝐵) ∈
V |
11 | | oveq1 6657 |
. . . . . 6
⊢ (𝑥 = (𝐴 ·𝑜 𝐵) → (𝑥 +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 𝐴)) |
12 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)) = (𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)) |
13 | | ovex 6678 |
. . . . . 6
⊢ ((𝐴 ·𝑜
𝐵) +𝑜
𝐴) ∈
V |
14 | 11, 12, 13 | fvmpt 6282 |
. . . . 5
⊢ ((𝐴 ·𝑜
𝐵) ∈ V → ((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴))‘(𝐴 ·𝑜 𝐵)) = ((𝐴 ·𝑜 𝐵) +𝑜 𝐴)) |
15 | 10, 14 | ax-mp 5 |
. . . 4
⊢ ((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴))‘(𝐴 ·𝑜 𝐵)) = ((𝐴 ·𝑜 𝐵) +𝑜 𝐴) |
16 | | nnon 7071 |
. . . . . . 7
⊢ (𝐵 ∈ ω → 𝐵 ∈ On) |
17 | | omv 7592 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅)‘𝐵)) |
18 | 16, 17 | sylan2 491 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜
𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅)‘𝐵)) |
19 | | fvres 6207 |
. . . . . . 7
⊢ (𝐵 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +𝑜
𝐴)), ∅) ↾
ω)‘𝐵) =
(rec((𝑥 ∈ V ↦
(𝑥 +𝑜
𝐴)), ∅)‘𝐵)) |
20 | 19 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) →
((rec((𝑥 ∈ V ↦
(𝑥 +𝑜
𝐴)), ∅) ↾
ω)‘𝐵) =
(rec((𝑥 ∈ V ↦
(𝑥 +𝑜
𝐴)), ∅)‘𝐵)) |
21 | 18, 20 | eqtr4d 2659 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜
𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅) ↾
ω)‘𝐵)) |
22 | 21 | fveq2d 6195 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → ((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴))‘(𝐴 ·𝑜 𝐵)) = ((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴))‘((rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅) ↾ ω)‘𝐵))) |
23 | 15, 22 | syl5eqr 2670 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜
𝐵) +𝑜
𝐴) = ((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴))‘((rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅) ↾ ω)‘𝐵))) |
24 | | frsuc 7532 |
. . . 4
⊢ (𝐵 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +𝑜
𝐴)), ∅) ↾
ω)‘suc 𝐵) =
((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴))‘((rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅) ↾
ω)‘𝐵))) |
25 | 24 | adantl 482 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) →
((rec((𝑥 ∈ V ↦
(𝑥 +𝑜
𝐴)), ∅) ↾
ω)‘suc 𝐵) =
((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴))‘((rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅) ↾
ω)‘𝐵))) |
26 | 23, 25 | eqtr4d 2659 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜
𝐵) +𝑜
𝐴) = ((rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅) ↾
ω)‘suc 𝐵)) |
27 | 9, 26 | eqtr4d 2659 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜
suc 𝐵) = ((𝐴 ·𝑜
𝐵) +𝑜
𝐴)) |