Theorem oa1suc

Description: Addition with 1 is same as successor. Proposition 4.34(a) of Mendelson p. 266. (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 )