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 syl5eqr ⊢ 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