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

Metamath Proof Explorer

Theorem oa1suc

Description: Addition with 1 is same as successor. Proposition 4.34(a) of Mendelson p. 266. Remark 2.4 of Schloeder p. 4. (Contributed by NM, 29-Oct-1995) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion oa1suc 
|- ( A e. On -> ( A +o 1o ) = suc A )

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 1 oveq2i 
 |-  ( A +o 1o ) = ( A +o suc (/) )
3 peano1 
 |-  (/) e. _om
4 onasuc 
 |-  ( ( A e. On /\ (/) e. _om ) -> ( A +o suc (/) ) = suc ( A +o (/) ) )
5 3 4 mpan2 
 |-  ( A e. On -> ( A +o suc (/) ) = suc ( A +o (/) ) )
6 2 5 eqtrid 
 |-  ( A e. On -> ( A +o 1o ) = suc ( A +o (/) ) )
7 oa0 
 |-  ( A e. On -> ( A +o (/) ) = A )
8 suceq 
 |-  ( ( A +o (/) ) = A -> suc ( A +o (/) ) = suc A )
9 7 8 syl 
 |-  ( A e. On -> suc ( A +o (/) ) = suc A )
10 6 9 eqtrd 
 |-  ( A e. On -> ( A +o 1o ) = suc A )