Theorem 1oequni2o

Description: The ordinal number 1o is the predecessor of the ordinal number 2o . (Contributed by ML, 19-Oct-2020)

	Ref	Expression
Assertion	1oequni2o	$$⊢1_{𝑜}=\bigcup 2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
2		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
3		2on0	$$⊢2_{𝑜}\ne \varnothing$$
4		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
5		nnlim	$$⊢2_{𝑜}\in \mathrm{\omega }\to \neg \mathrm{Lim}{2}_{𝑜}$$
6	4 5	ax-mp	$$⊢\neg \mathrm{Lim}{2}_{𝑜}$$
7		onsucuni3	$$⊢\left(2_{𝑜}\in \mathrm{On}\wedge 2_{𝑜}\ne \varnothing \wedge \neg \mathrm{Lim}{2}_{𝑜}\right)\to 2_{𝑜}=\mathrm{suc}\bigcup 2_{𝑜}$$
8	2 3 6 7	mp3an	$$⊢2_{𝑜}=\mathrm{suc}\bigcup 2_{𝑜}$$
9	1 8	eqtr3i	$$⊢\mathrm{suc}{1}_{𝑜}=\mathrm{suc}\bigcup 2_{𝑜}$$
10		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
11		onuni	$$⊢2_{𝑜}\in \mathrm{On}\to \bigcup 2_{𝑜}\in \mathrm{On}$$
12	2 11	ax-mp	$$⊢\bigcup 2_{𝑜}\in \mathrm{On}$$
13		suc11	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge \bigcup 2_{𝑜}\in \mathrm{On}\right)\to \left(\mathrm{suc}{1}_{𝑜}=\mathrm{suc}\bigcup 2_{𝑜}\leftrightarrow 1_{𝑜}=\bigcup 2_{𝑜}\right)$$
14	10 12 13	mp2an	$$⊢\mathrm{suc}{1}_{𝑜}=\mathrm{suc}\bigcup 2_{𝑜}\leftrightarrow 1_{𝑜}=\bigcup 2_{𝑜}$$
15	9 14	mpbi	$$⊢1_{𝑜}=\bigcup 2_{𝑜}$$