Metamath Proof Explorer

Theorem naddonnn

Description: Natural addition with a natural number on the right results in a value equal to that of ordinal addition. (Contributed by RP, 1-Jan-2025)

Ref Expression
Assertion naddonnn 
|- ( ( A e. On /\ B e. _om ) -> ( A +o B ) = ( A +no B ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( A +o x ) = ( A +o (/) ) )
2 oveq2 
 |-  ( x = (/) -> ( A +no x ) = ( A +no (/) ) )
3 1 2 eqeq12d 
 |-  ( x = (/) -> ( ( A +o x ) = ( A +no x ) <-> ( A +o (/) ) = ( A +no (/) ) ) )
4 3 imbi2d 
 |-  ( x = (/) -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o (/) ) = ( A +no (/) ) ) ) )
5 oveq2 
 |-  ( x = y -> ( A +o x ) = ( A +o y ) )
6 oveq2 
 |-  ( x = y -> ( A +no x ) = ( A +no y ) )
7 5 6 eqeq12d 
 |-  ( x = y -> ( ( A +o x ) = ( A +no x ) <-> ( A +o y ) = ( A +no y ) ) )
8 7 imbi2d 
 |-  ( x = y -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o y ) = ( A +no y ) ) ) )
9 oveq2 
 |-  ( x = suc y -> ( A +o x ) = ( A +o suc y ) )
10 oveq2 
 |-  ( x = suc y -> ( A +no x ) = ( A +no suc y ) )
11 9 10 eqeq12d 
 |-  ( x = suc y -> ( ( A +o x ) = ( A +no x ) <-> ( A +o suc y ) = ( A +no suc y ) ) )
12 11 imbi2d 
 |-  ( x = suc y -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o suc y ) = ( A +no suc y ) ) ) )
13 oveq2 
 |-  ( x = B -> ( A +o x ) = ( A +o B ) )
14 oveq2 
 |-  ( x = B -> ( A +no x ) = ( A +no B ) )
15 13 14 eqeq12d 
 |-  ( x = B -> ( ( A +o x ) = ( A +no x ) <-> ( A +o B ) = ( A +no B ) ) )
16 15 imbi2d 
 |-  ( x = B -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o B ) = ( A +no B ) ) ) )
17 oa0 
 |-  ( A e. On -> ( A +o (/) ) = A )
18 naddrid 
 |-  ( A e. On -> ( A +no (/) ) = A )
19 17 18 eqtr4d 
 |-  ( A e. On -> ( A +o (/) ) = ( A +no (/) ) )
20 nnon 
 |-  ( y e. _om -> y e. On )
21 suceq 
 |-  ( ( A +o y ) = ( A +no y ) -> suc ( A +o y ) = suc ( A +no y ) )
22 21 adantl 
 |-  ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> suc ( A +o y ) = suc ( A +no y ) )
23 oasuc 
 |-  ( ( A e. On /\ y e. On ) -> ( A +o suc y ) = suc ( A +o y ) )
24 23 adantr 
 |-  ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> ( A +o suc y ) = suc ( A +o y ) )
25 naddsuc2 
 |-  ( ( A e. On /\ y e. On ) -> ( A +no suc y ) = suc ( A +no y ) )
26 25 adantr 
 |-  ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> ( A +no suc y ) = suc ( A +no y ) )
27 22 24 26 3eqtr4d 
 |-  ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> ( A +o suc y ) = ( A +no suc y ) )
28 27 ex 
 |-  ( ( A e. On /\ y e. On ) -> ( ( A +o y ) = ( A +no y ) -> ( A +o suc y ) = ( A +no suc y ) ) )
29 28 expcom 
 |-  ( y e. On -> ( A e. On -> ( ( A +o y ) = ( A +no y ) -> ( A +o suc y ) = ( A +no suc y ) ) ) )
30 20 29 syl 
 |-  ( y e. _om -> ( A e. On -> ( ( A +o y ) = ( A +no y ) -> ( A +o suc y ) = ( A +no suc y ) ) ) )
31 30 a2d 
 |-  ( y e. _om -> ( ( A e. On -> ( A +o y ) = ( A +no y ) ) -> ( A e. On -> ( A +o suc y ) = ( A +no suc y ) ) ) )
32 4 8 12 16 19 31 finds 
 |-  ( B e. _om -> ( A e. On -> ( A +o B ) = ( A +no B ) ) )
33 32 impcom 
 |-  ( ( A e. On /\ B e. _om ) -> ( A +o B ) = ( A +no B ) )