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