Theorem naddoa

Description: Natural addition of a natural is the same as regular addition. (Contributed by Scott Fenton, 20-Aug-2025)

	Ref	Expression
Assertion	naddoa	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{\omega }\right)\to A+B=A{+}_{𝑜}B$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢y=\varnothing \to A+y=A+\varnothing$$
2		oveq2	$$⊢y=\varnothing \to A{+}_{𝑜}y=A{+}_{𝑜}\varnothing$$
3	1 2	eqeq12d	$$⊢y=\varnothing \to \left(A+y=A{+}_{𝑜}y\leftrightarrow A+\varnothing =A{+}_{𝑜}\varnothing \right)$$
4	3	imbi2d	$$⊢y=\varnothing \to \left(\left(A\in \mathrm{On}\to A+y=A{+}_{𝑜}y\right)\leftrightarrow \left(A\in \mathrm{On}\to A+\varnothing =A{+}_{𝑜}\varnothing \right)\right)$$
5		oveq2	$$⊢y=x\to A+y=A+x$$
6		oveq2	$$⊢y=x\to A{+}_{𝑜}y=A{+}_{𝑜}x$$
7	5 6	eqeq12d	$$⊢y=x\to \left(A+y=A{+}_{𝑜}y\leftrightarrow A+x=A{+}_{𝑜}x\right)$$
8	7	imbi2d	$$⊢y=x\to \left(\left(A\in \mathrm{On}\to A+y=A{+}_{𝑜}y\right)\leftrightarrow \left(A\in \mathrm{On}\to A+x=A{+}_{𝑜}x\right)\right)$$
9		oveq2	$$⊢y=\mathrm{suc}x\to A+y=A+\mathrm{suc}x$$
10		oveq2	$$⊢y=\mathrm{suc}x\to A{+}_{𝑜}y=A{+}_{𝑜}\mathrm{suc}x$$
11	9 10	eqeq12d	$$⊢y=\mathrm{suc}x\to \left(A+y=A{+}_{𝑜}y\leftrightarrow A+\mathrm{suc}x=A{+}_{𝑜}\mathrm{suc}x\right)$$
12	11	imbi2d	$$⊢y=\mathrm{suc}x\to \left(\left(A\in \mathrm{On}\to A+y=A{+}_{𝑜}y\right)\leftrightarrow \left(A\in \mathrm{On}\to A+\mathrm{suc}x=A{+}_{𝑜}\mathrm{suc}x\right)\right)$$
13		oveq2	$$⊢y=B\to A+y=A+B$$
14		oveq2	$$⊢y=B\to A{+}_{𝑜}y=A{+}_{𝑜}B$$
15	13 14	eqeq12d	$$⊢y=B\to \left(A+y=A{+}_{𝑜}y\leftrightarrow A+B=A{+}_{𝑜}B\right)$$
16	15	imbi2d	$$⊢y=B\to \left(\left(A\in \mathrm{On}\to A+y=A{+}_{𝑜}y\right)\leftrightarrow \left(A\in \mathrm{On}\to A+B=A{+}_{𝑜}B\right)\right)$$
17		naddrid	$$⊢A\in \mathrm{On}\to A+\varnothing =A$$
18		oa0	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}\varnothing =A$$
19	17 18	eqtr4d	$$⊢A\in \mathrm{On}\to A+\varnothing =A{+}_{𝑜}\varnothing$$
20		suceq	$$⊢A+x=A{+}_{𝑜}x\to \mathrm{suc}\left(A+x\right)=\mathrm{suc}\left(A{+}_{𝑜}x\right)$$
21	20	3ad2ant3	$$⊢\left(x\in \mathrm{\omega }\wedge A\in \mathrm{On}\wedge A+x=A{+}_{𝑜}x\right)\to \mathrm{suc}\left(A+x\right)=\mathrm{suc}\left(A{+}_{𝑜}x\right)$$
22		nnon	$$⊢x\in \mathrm{\omega }\to x\in \mathrm{On}$$
23		naddsuc2	$$⊢\left(A\in \mathrm{On}\wedge x\in \mathrm{On}\right)\to A+\mathrm{suc}x=\mathrm{suc}\left(A+x\right)$$
24	22 23	sylan2	$$⊢\left(A\in \mathrm{On}\wedge x\in \mathrm{\omega }\right)\to A+\mathrm{suc}x=\mathrm{suc}\left(A+x\right)$$
25	24	ancoms	$$⊢\left(x\in \mathrm{\omega }\wedge A\in \mathrm{On}\right)\to A+\mathrm{suc}x=\mathrm{suc}\left(A+x\right)$$
26	25	3adant3	$$⊢\left(x\in \mathrm{\omega }\wedge A\in \mathrm{On}\wedge A+x=A{+}_{𝑜}x\right)\to A+\mathrm{suc}x=\mathrm{suc}\left(A+x\right)$$
27		onasuc	$$⊢\left(A\in \mathrm{On}\wedge x\in \mathrm{\omega }\right)\to A{+}_{𝑜}\mathrm{suc}x=\mathrm{suc}\left(A{+}_{𝑜}x\right)$$
28	27	ancoms	$$⊢\left(x\in \mathrm{\omega }\wedge A\in \mathrm{On}\right)\to A{+}_{𝑜}\mathrm{suc}x=\mathrm{suc}\left(A{+}_{𝑜}x\right)$$
29	28	3adant3	$$⊢\left(x\in \mathrm{\omega }\wedge A\in \mathrm{On}\wedge A+x=A{+}_{𝑜}x\right)\to A{+}_{𝑜}\mathrm{suc}x=\mathrm{suc}\left(A{+}_{𝑜}x\right)$$
30	21 26 29	3eqtr4d	$$⊢\left(x\in \mathrm{\omega }\wedge A\in \mathrm{On}\wedge A+x=A{+}_{𝑜}x\right)\to A+\mathrm{suc}x=A{+}_{𝑜}\mathrm{suc}x$$
31	30	3exp	$$⊢x\in \mathrm{\omega }\to \left(A\in \mathrm{On}\to \left(A+x=A{+}_{𝑜}x\to A+\mathrm{suc}x=A{+}_{𝑜}\mathrm{suc}x\right)\right)$$
32	31	a2d	$$⊢x\in \mathrm{\omega }\to \left(\left(A\in \mathrm{On}\to A+x=A{+}_{𝑜}x\right)\to \left(A\in \mathrm{On}\to A+\mathrm{suc}x=A{+}_{𝑜}\mathrm{suc}x\right)\right)$$
33	4 8 12 16 19 32	finds	$$⊢B\in \mathrm{\omega }\to \left(A\in \mathrm{On}\to A+B=A{+}_{𝑜}B\right)$$
34	33	impcom	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{\omega }\right)\to A+B=A{+}_{𝑜}B$$