Theorem oa0r

Description: Ordinal addition with zero. Proposition 8.3 of TakeutiZaring p. 57. (Contributed by NM, 5-May-1995)

	Ref	Expression
Assertion	oa0r	$$⊢A\in \mathrm{On}\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		oasuc	$$⊢\left(\varnothing \in \mathrm{On}\wedge y\in \mathrm{On}\right)\to \varnothing {+}_{𝑜}\mathrm{suc}y=\mathrm{suc}\left(\varnothing {+}_{𝑜}y\right)$$
17	13 16	mpan	$$⊢y\in \mathrm{On}\to \varnothing {+}_{𝑜}\mathrm{suc}y=\mathrm{suc}\left(\varnothing {+}_{𝑜}y\right)$$
18		suceq	$$⊢\varnothing {+}_{𝑜}y=y\to \mathrm{suc}\left(\varnothing {+}_{𝑜}y\right)=\mathrm{suc}y$$
19	17 18	sylan9eq	$$⊢\left(y\in \mathrm{On}\wedge \varnothing {+}_{𝑜}y=y\right)\to \varnothing {+}_{𝑜}\mathrm{suc}y=\mathrm{suc}y$$
20	19	ex	$$⊢y\in \mathrm{On}\to \left(\varnothing {+}_{𝑜}y=y\to \varnothing {+}_{𝑜}\mathrm{suc}y=\mathrm{suc}y\right)$$
21		iuneq2	$$⊢\forall y\in x\varnothing {+}_{𝑜}y=y\to \bigcup _{y\in x}\left(\varnothing {+}_{𝑜}y\right)=\bigcup _{y\in x}y$$
22		uniiun	$$⊢\bigcup x=\bigcup _{y\in x}y$$
23	21 22	eqtr4di	$$⊢\forall y\in x\varnothing {+}_{𝑜}y=y\to \bigcup _{y\in x}\left(\varnothing {+}_{𝑜}y\right)=\bigcup x$$
24		vex	$$⊢x\in \mathrm{V}$$
25		oalim	$$⊢\left(\varnothing \in \mathrm{On}\wedge \left(x\in \mathrm{V}\wedge \mathrm{Lim}x\right)\right)\to \varnothing {+}_{𝑜}x=\bigcup _{y\in x}\left(\varnothing {+}_{𝑜}y\right)$$
26	13 25	mpan	$$⊢\left(x\in \mathrm{V}\wedge \mathrm{Lim}x\right)\to \varnothing {+}_{𝑜}x=\bigcup _{y\in x}\left(\varnothing {+}_{𝑜}y\right)$$
27	24 26	mpan	$$⊢\mathrm{Lim}x\to \varnothing {+}_{𝑜}x=\bigcup _{y\in x}\left(\varnothing {+}_{𝑜}y\right)$$
28		limuni	$$⊢\mathrm{Lim}x\to x=\bigcup x$$
29	27 28	eqeq12d	$$⊢\mathrm{Lim}x\to \left(\varnothing {+}_{𝑜}x=x\leftrightarrow \bigcup _{y\in x}\left(\varnothing {+}_{𝑜}y\right)=\bigcup x\right)$$
30	23 29	syl5ibr	$$⊢\mathrm{Lim}x\to \left(\forall y\in x\varnothing {+}_{𝑜}y=y\to \varnothing {+}_{𝑜}x=x\right)$$
31	3 6 9 12 15 20 30	tfinds	$$⊢A\in \mathrm{On}\to \varnothing {+}_{𝑜}A=A$$