Theorem nlim2

Description: 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024)

	Ref	Expression
Assertion	nlim2	$$⊢\neg \mathrm{Lim}{2}_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
2	1	prid2	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
3		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
4	2 3	eleqtrri	$$⊢1_{𝑜}\in 2_{𝑜}$$
5		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
6	5	onirri	$$⊢\neg 1_{𝑜}\in 1_{𝑜}$$
7		eleq2	$$⊢2_{𝑜}=1_{𝑜}\to \left(1_{𝑜}\in 2_{𝑜}\leftrightarrow 1_{𝑜}\in 1_{𝑜}\right)$$
8	6 7	mtbiri	$$⊢2_{𝑜}=1_{𝑜}\to \neg 1_{𝑜}\in 2_{𝑜}$$
9	4 8	mt2	$$⊢\neg 2_{𝑜}=1_{𝑜}$$
10	9	neir	$$⊢2_{𝑜}\ne 1_{𝑜}$$
11	3	unieqi	$$⊢\bigcup 2_{𝑜}=\bigcup \left\{\varnothing ,1_{𝑜}\right\}$$
12		0ex	$$⊢\varnothing \in \mathrm{V}$$
13	12 1	unipr	$$⊢\bigcup \left\{\varnothing ,1_{𝑜}\right\}=\varnothing \cup 1_{𝑜}$$
14		0un	$$⊢\varnothing \cup 1_{𝑜}=1_{𝑜}$$
15	11 13 14	3eqtri	$$⊢\bigcup 2_{𝑜}=1_{𝑜}$$
16	10 15	neeqtrri	$$⊢2_{𝑜}\ne \bigcup 2_{𝑜}$$
17	16	neii	$$⊢\neg 2_{𝑜}=\bigcup 2_{𝑜}$$
18		simp3	$$⊢\left(\mathrm{Ord}{2}_{𝑜}\wedge 2_{𝑜}\ne \varnothing \wedge 2_{𝑜}=\bigcup 2_{𝑜}\right)\to 2_{𝑜}=\bigcup 2_{𝑜}$$
19	17 18	mto	$$⊢\neg \left(\mathrm{Ord}{2}_{𝑜}\wedge 2_{𝑜}\ne \varnothing \wedge 2_{𝑜}=\bigcup 2_{𝑜}\right)$$
20		df-lim	$$⊢\mathrm{Lim}{2}_{𝑜}\leftrightarrow \left(\mathrm{Ord}{2}_{𝑜}\wedge 2_{𝑜}\ne \varnothing \wedge 2_{𝑜}=\bigcup 2_{𝑜}\right)$$
21	19 20	mtbir	$$⊢\neg \mathrm{Lim}{2}_{𝑜}$$