Theorem naddonnn

Description: Natural addition with a natural number on the right results in a value equal to that of ordinal addition. (Contributed by RP, 1-Jan-2025)

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

Proof

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