Theorem om1r

Description: Ordinal multiplication with 1. Proposition 8.18(2) of TakeutiZaring p. 63. Lemma 2.15 of Schloeder p. 5. (Contributed by NM, 3-Aug-2004)

	Ref	Expression
Assertion	om1r	$$⊢A\in \mathrm{On}\to 1_{𝑜}{\cdot }_{𝑜}A=A$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=\varnothing \to 1_{𝑜}{\cdot }_{𝑜}x=1_{𝑜}{\cdot }_{𝑜}\varnothing$$
2		id	$$⊢x=\varnothing \to x=\varnothing$$
3	1 2	eqeq12d	$$⊢x=\varnothing \to \left(1_{𝑜}{\cdot }_{𝑜}x=x\leftrightarrow 1_{𝑜}{\cdot }_{𝑜}\varnothing =\varnothing \right)$$
4		oveq2	$$⊢x=y\to 1_{𝑜}{\cdot }_{𝑜}x=1_{𝑜}{\cdot }_{𝑜}y$$
5		id	$$⊢x=y\to x=y$$
6	4 5	eqeq12d	$$⊢x=y\to \left(1_{𝑜}{\cdot }_{𝑜}x=x\leftrightarrow 1_{𝑜}{\cdot }_{𝑜}y=y\right)$$
7		oveq2	$$⊢x=\mathrm{suc}y\to 1_{𝑜}{\cdot }_{𝑜}x=1_{𝑜}{\cdot }_{𝑜}\mathrm{suc}y$$
8		id	$$⊢x=\mathrm{suc}y\to x=\mathrm{suc}y$$
9	7 8	eqeq12d	$$⊢x=\mathrm{suc}y\to \left(1_{𝑜}{\cdot }_{𝑜}x=x\leftrightarrow 1_{𝑜}{\cdot }_{𝑜}\mathrm{suc}y=\mathrm{suc}y\right)$$
10		oveq2	$$⊢x=A\to 1_{𝑜}{\cdot }_{𝑜}x=1_{𝑜}{\cdot }_{𝑜}A$$
11		id	$$⊢x=A\to x=A$$
12	10 11	eqeq12d	$$⊢x=A\to \left(1_{𝑜}{\cdot }_{𝑜}x=x\leftrightarrow 1_{𝑜}{\cdot }_{𝑜}A=A\right)$$
13		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
14		om0	$$⊢1_{𝑜}\in \mathrm{On}\to 1_{𝑜}{\cdot }_{𝑜}\varnothing =\varnothing$$
15	13 14	ax-mp	$$⊢1_{𝑜}{\cdot }_{𝑜}\varnothing =\varnothing$$
16		omsuc	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge y\in \mathrm{On}\right)\to 1_{𝑜}{\cdot }_{𝑜}\mathrm{suc}y=\left(1_{𝑜}{\cdot }_{𝑜}y\right){+}_{𝑜}{1}_{𝑜}$$
17	13 16	mpan	$$⊢y\in \mathrm{On}\to 1_{𝑜}{\cdot }_{𝑜}\mathrm{suc}y=\left(1_{𝑜}{\cdot }_{𝑜}y\right){+}_{𝑜}{1}_{𝑜}$$
18		oveq1	$$⊢1_{𝑜}{\cdot }_{𝑜}y=y\to \left(1_{𝑜}{\cdot }_{𝑜}y\right){+}_{𝑜}{1}_{𝑜}=y{+}_{𝑜}{1}_{𝑜}$$
19	17 18	sylan9eq	$$⊢\left(y\in \mathrm{On}\wedge 1_{𝑜}{\cdot }_{𝑜}y=y\right)\to 1_{𝑜}{\cdot }_{𝑜}\mathrm{suc}y=y{+}_{𝑜}{1}_{𝑜}$$
20		oa1suc	$$⊢y\in \mathrm{On}\to y{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}y$$
21	20	adantr	$$⊢\left(y\in \mathrm{On}\wedge 1_{𝑜}{\cdot }_{𝑜}y=y\right)\to y{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}y$$
22	19 21	eqtrd	$$⊢\left(y\in \mathrm{On}\wedge 1_{𝑜}{\cdot }_{𝑜}y=y\right)\to 1_{𝑜}{\cdot }_{𝑜}\mathrm{suc}y=\mathrm{suc}y$$
23	22	ex	$$⊢y\in \mathrm{On}\to \left(1_{𝑜}{\cdot }_{𝑜}y=y\to 1_{𝑜}{\cdot }_{𝑜}\mathrm{suc}y=\mathrm{suc}y\right)$$
24		iuneq2	$$⊢\forall y\in x{1}_{𝑜}{\cdot }_{𝑜}y=y\to \bigcup _{y\in x}\left(1_{𝑜}{\cdot }_{𝑜}y\right)=\bigcup _{y\in x}y$$
25		uniiun	$$⊢\bigcup x=\bigcup _{y\in x}y$$
26	24 25	eqtr4di	$$⊢\forall y\in x{1}_{𝑜}{\cdot }_{𝑜}y=y\to \bigcup _{y\in x}\left(1_{𝑜}{\cdot }_{𝑜}y\right)=\bigcup x$$
27		vex	$$⊢x\in \mathrm{V}$$
28		omlim	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge \left(x\in \mathrm{V}\wedge \mathrm{Lim}x\right)\right)\to 1_{𝑜}{\cdot }_{𝑜}x=\bigcup _{y\in x}\left(1_{𝑜}{\cdot }_{𝑜}y\right)$$
29	13 28	mpan	$$⊢\left(x\in \mathrm{V}\wedge \mathrm{Lim}x\right)\to 1_{𝑜}{\cdot }_{𝑜}x=\bigcup _{y\in x}\left(1_{𝑜}{\cdot }_{𝑜}y\right)$$
30	27 29	mpan	$$⊢\mathrm{Lim}x\to 1_{𝑜}{\cdot }_{𝑜}x=\bigcup _{y\in x}\left(1_{𝑜}{\cdot }_{𝑜}y\right)$$
31		limuni	$$⊢\mathrm{Lim}x\to x=\bigcup x$$
32	30 31	eqeq12d	$$⊢\mathrm{Lim}x\to \left(1_{𝑜}{\cdot }_{𝑜}x=x\leftrightarrow \bigcup _{y\in x}\left(1_{𝑜}{\cdot }_{𝑜}y\right)=\bigcup x\right)$$
33	26 32	imbitrrid	$$⊢\mathrm{Lim}x\to \left(\forall y\in x{1}_{𝑜}{\cdot }_{𝑜}y=y\to 1_{𝑜}{\cdot }_{𝑜}x=x\right)$$
34	3 6 9 12 15 23 33	tfinds	$$⊢A\in \mathrm{On}\to 1_{𝑜}{\cdot }_{𝑜}A=A$$