This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )