Metamath Proof Explorer

Theorem onmsuc

Description: Multiplication with successor. Theorem 4J(A2) of Enderton p. 80. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion onmsuc ⊢A∈On∧B∈ω→A⋅𝑜suc⁡B=A⋅𝑜B+𝑜A

Proof

Step Hyp Ref Expression
1 peano2 ⊢B∈ω→suc⁡B∈ω
2 nnon ⊢suc⁡B∈ω→suc⁡B∈On
3 1 2 syl ⊢B∈ω→suc⁡B∈On
4 omv ⊢A∈On∧suc⁡B∈On→A⋅𝑜suc⁡B=rec⁡x∈V⟼x+𝑜A∅⁡suc⁡B
5 3 4 sylan2 ⊢A∈On∧B∈ω→A⋅𝑜suc⁡B=rec⁡x∈V⟼x+𝑜A∅⁡suc⁡B
6 1 adantl ⊢A∈On∧B∈ω→suc⁡B∈ω
7 6 fvresd ⊢A∈On∧B∈ω→rec⁡x∈V⟼x+𝑜A∅↾ω⁡suc⁡B=rec⁡x∈V⟼x+𝑜A∅⁡suc⁡B
8 5 7 eqtr4d ⊢A∈On∧B∈ω→A⋅𝑜suc⁡B=rec⁡x∈V⟼x+𝑜A∅↾ω⁡suc⁡B
9 ovex ⊢A⋅𝑜B∈V
10 oveq1 ⊢x=A⋅𝑜B→x+𝑜A=A⋅𝑜B+𝑜A
11 eqid ⊢x∈V⟼x+𝑜A=x∈V⟼x+𝑜A
12 ovex ⊢A⋅𝑜B+𝑜A∈V
13 10 11 12 fvmpt ⊢A⋅𝑜B∈V→x∈V⟼x+𝑜A⁡A⋅𝑜B=A⋅𝑜B+𝑜A
14 9 13 ax-mp ⊢x∈V⟼x+𝑜A⁡A⋅𝑜B=A⋅𝑜B+𝑜A
15 nnon ⊢B∈ω→B∈On
16 omv ⊢A∈On∧B∈On→A⋅𝑜B=rec⁡x∈V⟼x+𝑜A∅⁡B
17 15 16 sylan2 ⊢A∈On∧B∈ω→A⋅𝑜B=rec⁡x∈V⟼x+𝑜A∅⁡B
18 fvres ⊢B∈ω→rec⁡x∈V⟼x+𝑜A∅↾ω⁡B=rec⁡x∈V⟼x+𝑜A∅⁡B
19 18 adantl ⊢A∈On∧B∈ω→rec⁡x∈V⟼x+𝑜A∅↾ω⁡B=rec⁡x∈V⟼x+𝑜A∅⁡B
20 17 19 eqtr4d ⊢A∈On∧B∈ω→A⋅𝑜B=rec⁡x∈V⟼x+𝑜A∅↾ω⁡B
21 20 fveq2d ⊢A∈On∧B∈ω→x∈V⟼x+𝑜A⁡A⋅𝑜B=x∈V⟼x+𝑜A⁡rec⁡x∈V⟼x+𝑜A∅↾ω⁡B
22 14 21 eqtr3id ⊢A∈On∧B∈ω→A⋅𝑜B+𝑜A=x∈V⟼x+𝑜A⁡rec⁡x∈V⟼x+𝑜A∅↾ω⁡B
23 frsuc ⊢B∈ω→rec⁡x∈V⟼x+𝑜A∅↾ω⁡suc⁡B=x∈V⟼x+𝑜A⁡rec⁡x∈V⟼x+𝑜A∅↾ω⁡B
24 23 adantl ⊢A∈On∧B∈ω→rec⁡x∈V⟼x+𝑜A∅↾ω⁡suc⁡B=x∈V⟼x+𝑜A⁡rec⁡x∈V⟼x+𝑜A∅↾ω⁡B
25 22 24 eqtr4d ⊢A∈On∧B∈ω→A⋅𝑜B+𝑜A=rec⁡x∈V⟼x+𝑜A∅↾ω⁡suc⁡B
26 8 25 eqtr4d ⊢A∈On∧B∈ω→A⋅𝑜suc⁡B=A⋅𝑜B+𝑜A