Metamath Proof Explorer

Theorem nna0r

Description: Addition to zero. Remark in proof of Theorem 4K(2) of Enderton p. 81. Note: In this and later theorems, we deliberately avoid the more general ordinal versions of these theorems (in this case oa0r ) so that we can avoid ax-rep , which is not needed for finite recursive definitions. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion nna0r 
|- ( A e. _om -> ( (/) +o A ) = A )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( (/) +o x ) = ( (/) +o (/) ) )
2 id 
 |-  ( x = (/) -> x = (/) )
3 1 2 eqeq12d 
 |-  ( x = (/) -> ( ( (/) +o x ) = x <-> ( (/) +o (/) ) = (/) ) )
4 oveq2 
 |-  ( x = y -> ( (/) +o x ) = ( (/) +o y ) )
5 id 
 |-  ( x = y -> x = y )
6 4 5 eqeq12d 
 |-  ( x = y -> ( ( (/) +o x ) = x <-> ( (/) +o y ) = y ) )
7 oveq2 
 |-  ( x = suc y -> ( (/) +o x ) = ( (/) +o suc y ) )
8 id 
 |-  ( x = suc y -> x = suc y )
9 7 8 eqeq12d 
 |-  ( x = suc y -> ( ( (/) +o x ) = x <-> ( (/) +o suc y ) = suc y ) )
10 oveq2 
 |-  ( x = A -> ( (/) +o x ) = ( (/) +o A ) )
11 id 
 |-  ( x = A -> x = A )
12 10 11 eqeq12d 
 |-  ( x = A -> ( ( (/) +o x ) = x <-> ( (/) +o A ) = A ) )
13 0elon 
 |-  (/) e. On
14 oa0 
 |-  ( (/) e. On -> ( (/) +o (/) ) = (/) )
15 13 14 ax-mp 
 |-  ( (/) +o (/) ) = (/)
16 peano1 
 |-  (/) e. _om
17 nnasuc 
 |-  ( ( (/) e. _om /\ y e. _om ) -> ( (/) +o suc y ) = suc ( (/) +o y ) )
18 16 17 mpan 
 |-  ( y e. _om -> ( (/) +o suc y ) = suc ( (/) +o y ) )
19 suceq 
 |-  ( ( (/) +o y ) = y -> suc ( (/) +o y ) = suc y )
20 19 eqeq2d 
 |-  ( ( (/) +o y ) = y -> ( ( (/) +o suc y ) = suc ( (/) +o y ) <-> ( (/) +o suc y ) = suc y ) )
21 18 20 syl5ibcom 
 |-  ( y e. _om -> ( ( (/) +o y ) = y -> ( (/) +o suc y ) = suc y ) )
22 3 6 9 12 15 21 finds 
 |-  ( A e. _om -> ( (/) +o A ) = A )