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\in \mathrm{On}\to A{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
2	1	oveq2i	$$⊢A{+}_{𝑜}{1}_{𝑜}=A{+}_{𝑜}\mathrm{suc}\varnothing$$
3		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
4		onasuc	$$⊢\left(A\in \mathrm{On}\wedge \varnothing \in \mathrm{\omega }\right)\to A{+}_{𝑜}\mathrm{suc}\varnothing =\mathrm{suc}\left(A{+}_{𝑜}\varnothing \right)$$
5	3 4	mpan2	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}\mathrm{suc}\varnothing =\mathrm{suc}\left(A{+}_{𝑜}\varnothing \right)$$
6	2 5	eqtrid	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}\left(A{+}_{𝑜}\varnothing \right)$$
7		oa0	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}\varnothing =A$$
8		suceq	$$⊢A{+}_{𝑜}\varnothing =A\to \mathrm{suc}\left(A{+}_{𝑜}\varnothing \right)=\mathrm{suc}A$$
9	7 8	syl	$$⊢A\in \mathrm{On}\to \mathrm{suc}\left(A{+}_{𝑜}\varnothing \right)=\mathrm{suc}A$$
10	6 9	eqtrd	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}A$$