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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=\varnothing \to \varnothing {+}_{𝑜}x=\varnothing {+}_{𝑜}\varnothing$$
2		id	$$⊢x=\varnothing \to x=\varnothing$$
3	1 2	eqeq12d	$$⊢x=\varnothing \to \left(\varnothing {+}_{𝑜}x=x\leftrightarrow \varnothing {+}_{𝑜}\varnothing =\varnothing \right)$$
4		oveq2	$$⊢x=y\to \varnothing {+}_{𝑜}x=\varnothing {+}_{𝑜}y$$
5		id	$$⊢x=y\to x=y$$
6	4 5	eqeq12d	$$⊢x=y\to \left(\varnothing {+}_{𝑜}x=x\leftrightarrow \varnothing {+}_{𝑜}y=y\right)$$
7		oveq2	$$⊢x=\mathrm{suc}y\to \varnothing {+}_{𝑜}x=\varnothing {+}_{𝑜}\mathrm{suc}y$$
8		id	$$⊢x=\mathrm{suc}y\to x=\mathrm{suc}y$$
9	7 8	eqeq12d	$$⊢x=\mathrm{suc}y\to \left(\varnothing {+}_{𝑜}x=x\leftrightarrow \varnothing {+}_{𝑜}\mathrm{suc}y=\mathrm{suc}y\right)$$
10		oveq2	$$⊢x=A\to \varnothing {+}_{𝑜}x=\varnothing {+}_{𝑜}A$$
11		id	$$⊢x=A\to x=A$$
12	10 11	eqeq12d	$$⊢x=A\to \left(\varnothing {+}_{𝑜}x=x\leftrightarrow \varnothing {+}_{𝑜}A=A\right)$$
13		0elon	$$⊢\varnothing \in \mathrm{On}$$
14		oa0	$$⊢\varnothing \in \mathrm{On}\to \varnothing {+}_{𝑜}\varnothing =\varnothing$$
15	13 14	ax-mp	$$⊢\varnothing {+}_{𝑜}\varnothing =\varnothing$$
16		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
17		nnasuc	$$⊢\left(\varnothing \in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to \varnothing {+}_{𝑜}\mathrm{suc}y=\mathrm{suc}\left(\varnothing {+}_{𝑜}y\right)$$
18	16 17	mpan	$$⊢y\in \mathrm{\omega }\to \varnothing {+}_{𝑜}\mathrm{suc}y=\mathrm{suc}\left(\varnothing {+}_{𝑜}y\right)$$
19		suceq	$$⊢\varnothing {+}_{𝑜}y=y\to \mathrm{suc}\left(\varnothing {+}_{𝑜}y\right)=\mathrm{suc}y$$
20	19	eqeq2d	$$⊢\varnothing {+}_{𝑜}y=y\to \left(\varnothing {+}_{𝑜}\mathrm{suc}y=\mathrm{suc}\left(\varnothing {+}_{𝑜}y\right)\leftrightarrow \varnothing {+}_{𝑜}\mathrm{suc}y=\mathrm{suc}y\right)$$
21	18 20	syl5ibcom	$$⊢y\in \mathrm{\omega }\to \left(\varnothing {+}_{𝑜}y=y\to \varnothing {+}_{𝑜}\mathrm{suc}y=\mathrm{suc}y\right)$$
22	3 6 9 12 15 21	finds	$$⊢A\in \mathrm{\omega }\to \varnothing {+}_{𝑜}A=A$$