| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | frsuc 8478 | . . . 4
⊢ (𝐵 ∈ ω →
((rec((𝑥 ∈ V ↦
suc 𝑥), 𝐴) ↾ ω)‘suc 𝐵) = ((𝑥 ∈ V ↦ suc 𝑥)‘((rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴) ↾ ω)‘𝐵))) | 
| 2 | 1 | adantl 481 | . . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) →
((rec((𝑥 ∈ V ↦
suc 𝑥), 𝐴) ↾ ω)‘suc 𝐵) = ((𝑥 ∈ V ↦ suc 𝑥)‘((rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴) ↾ ω)‘𝐵))) | 
| 3 |  | peano2 7913 | . . . . 5
⊢ (𝐵 ∈ ω → suc 𝐵 ∈
ω) | 
| 4 | 3 | adantl 481 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → suc
𝐵 ∈
ω) | 
| 5 | 4 | fvresd 6925 | . . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) →
((rec((𝑥 ∈ V ↦
suc 𝑥), 𝐴) ↾ ω)‘suc 𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘suc 𝐵)) | 
| 6 |  | fvres 6924 | . . . . 5
⊢ (𝐵 ∈ ω →
((rec((𝑥 ∈ V ↦
suc 𝑥), 𝐴) ↾ ω)‘𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵)) | 
| 7 | 6 | adantl 481 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) →
((rec((𝑥 ∈ V ↦
suc 𝑥), 𝐴) ↾ ω)‘𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵)) | 
| 8 | 7 | fveq2d 6909 | . . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → ((𝑥 ∈ V ↦ suc 𝑥)‘((rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴) ↾ ω)‘𝐵)) = ((𝑥 ∈ V ↦ suc 𝑥)‘(rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵))) | 
| 9 | 2, 5, 8 | 3eqtr3d 2784 | . 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) →
(rec((𝑥 ∈ V ↦
suc 𝑥), 𝐴)‘suc 𝐵) = ((𝑥 ∈ V ↦ suc 𝑥)‘(rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵))) | 
| 10 |  | nnon 7894 | . . . 4
⊢ (𝐵 ∈ ω → 𝐵 ∈ On) | 
| 11 |  | onsuc 7832 | . . . 4
⊢ (𝐵 ∈ On → suc 𝐵 ∈ On) | 
| 12 | 10, 11 | syl 17 | . . 3
⊢ (𝐵 ∈ ω → suc 𝐵 ∈ On) | 
| 13 |  | oav 8550 | . . 3
⊢ ((𝐴 ∈ On ∧ suc 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘suc 𝐵)) | 
| 14 | 12, 13 | sylan2 593 | . 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘suc 𝐵)) | 
| 15 |  | ovex 7465 | . . . 4
⊢ (𝐴 +o 𝐵) ∈ V | 
| 16 |  | suceq 6449 | . . . . 5
⊢ (𝑥 = (𝐴 +o 𝐵) → suc 𝑥 = suc (𝐴 +o 𝐵)) | 
| 17 |  | eqid 2736 | . . . . 5
⊢ (𝑥 ∈ V ↦ suc 𝑥) = (𝑥 ∈ V ↦ suc 𝑥) | 
| 18 | 15 | sucex 7827 | . . . . 5
⊢ suc
(𝐴 +o 𝐵) ∈ V | 
| 19 | 16, 17, 18 | fvmpt 7015 | . . . 4
⊢ ((𝐴 +o 𝐵) ∈ V → ((𝑥 ∈ V ↦ suc 𝑥)‘(𝐴 +o 𝐵)) = suc (𝐴 +o 𝐵)) | 
| 20 | 15, 19 | ax-mp 5 | . . 3
⊢ ((𝑥 ∈ V ↦ suc 𝑥)‘(𝐴 +o 𝐵)) = suc (𝐴 +o 𝐵) | 
| 21 |  | oav 8550 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵)) | 
| 22 | 10, 21 | sylan2 593 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵)) | 
| 23 | 22 | fveq2d 6909 | . . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → ((𝑥 ∈ V ↦ suc 𝑥)‘(𝐴 +o 𝐵)) = ((𝑥 ∈ V ↦ suc 𝑥)‘(rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵))) | 
| 24 | 20, 23 | eqtr3id 2790 | . 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → suc
(𝐴 +o 𝐵) = ((𝑥 ∈ V ↦ suc 𝑥)‘(rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵))) | 
| 25 | 9, 14, 24 | 3eqtr4d 2786 | 1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) |