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 e. On /\ B e. _om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )

Proof

Step Hyp Ref Expression
1 peano2
 |-  ( B e. _om -> suc B e. _om )
2 nnon
 |-  ( suc B e. _om -> suc B e. On )
3 1 2 syl
 |-  ( B e. _om -> suc B e. On )
4 omv
 |-  ( ( A e. On /\ suc B e. On ) -> ( A .o suc B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` suc B ) )
5 3 4 sylan2
 |-  ( ( A e. On /\ B e. _om ) -> ( A .o suc B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` suc B ) )
6 1 adantl
 |-  ( ( A e. On /\ B e. _om ) -> suc B e. _om )
7 6 fvresd
 |-  ( ( A e. On /\ B e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` suc B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` suc B ) )
8 5 7 eqtr4d
 |-  ( ( A e. On /\ B e. _om ) -> ( A .o suc B ) = ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` suc B ) )
9 ovex
 |-  ( A .o B ) e. _V
10 oveq1
 |-  ( x = ( A .o B ) -> ( x +o A ) = ( ( A .o B ) +o A ) )
11 eqid
 |-  ( x e. _V |-> ( x +o A ) ) = ( x e. _V |-> ( x +o A ) )
12 ovex
 |-  ( ( A .o B ) +o A ) e. _V
13 10 11 12 fvmpt
 |-  ( ( A .o B ) e. _V -> ( ( x e. _V |-> ( x +o A ) ) ` ( A .o B ) ) = ( ( A .o B ) +o A ) )
14 9 13 ax-mp
 |-  ( ( x e. _V |-> ( x +o A ) ) ` ( A .o B ) ) = ( ( A .o B ) +o A )
15 nnon
 |-  ( B e. _om -> B e. On )
16 omv
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) )
17 15 16 sylan2
 |-  ( ( A e. On /\ B e. _om ) -> ( A .o B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) )
18 fvres
 |-  ( B e. _om -> ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) )
19 18 adantl
 |-  ( ( A e. On /\ B e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) )
20 17 19 eqtr4d
 |-  ( ( A e. On /\ B e. _om ) -> ( A .o B ) = ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` B ) )
21 20 fveq2d
 |-  ( ( A e. On /\ B e. _om ) -> ( ( x e. _V |-> ( x +o A ) ) ` ( A .o B ) ) = ( ( x e. _V |-> ( x +o A ) ) ` ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` B ) ) )
22 14 21 eqtr3id
 |-  ( ( A e. On /\ B e. _om ) -> ( ( A .o B ) +o A ) = ( ( x e. _V |-> ( x +o A ) ) ` ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` B ) ) )
23 frsuc
 |-  ( B e. _om -> ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` suc B ) = ( ( x e. _V |-> ( x +o A ) ) ` ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` B ) ) )
24 23 adantl
 |-  ( ( A e. On /\ B e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` suc B ) = ( ( x e. _V |-> ( x +o A ) ) ` ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` B ) ) )
25 22 24 eqtr4d
 |-  ( ( A e. On /\ B e. _om ) -> ( ( A .o B ) +o A ) = ( ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) |` _om ) ` suc B ) )
26 8 25 eqtr4d
 |-  ( ( A e. On /\ B e. _om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )