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	⊢ ( 𝐴 ∈ On → ( 𝐴 +o 1o ) = suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-1o	⊢ 1o = suc ∅
2	1	oveq2i	⊢ ( 𝐴 +o 1o ) = ( 𝐴 +o suc ∅ )
3		peano1	⊢ ∅ ∈ ω
4		onasuc	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ω ) → ( 𝐴 +o suc ∅ ) = suc ( 𝐴 +o ∅ ) )
5	3 4	mpan2	⊢ ( 𝐴 ∈ On → ( 𝐴 +o suc ∅ ) = suc ( 𝐴 +o ∅ ) )
6	2 5	eqtrid	⊢ ( 𝐴 ∈ On → ( 𝐴 +o 1o ) = suc ( 𝐴 +o ∅ ) )
7		oa0	⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = 𝐴 )
8		suceq	⊢ ( ( 𝐴 +o ∅ ) = 𝐴 → suc ( 𝐴 +o ∅ ) = suc 𝐴 )
9	7 8	syl	⊢ ( 𝐴 ∈ On → suc ( 𝐴 +o ∅ ) = suc 𝐴 )
10	6 9	eqtrd	⊢ ( 𝐴 ∈ On → ( 𝐴 +o 1o ) = suc 𝐴 )