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		1oelpr	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
2		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
3	1 2	eleqtrri	$$⊢1_{𝑜}\in 2_{𝑜}$$
4		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
5	4	onirri	$$⊢\neg 1_{𝑜}\in 1_{𝑜}$$
6		eleq2	$$⊢2_{𝑜}=1_{𝑜}\to \left(1_{𝑜}\in 2_{𝑜}\leftrightarrow 1_{𝑜}\in 1_{𝑜}\right)$$
7	5 6	mtbiri	$$⊢2_{𝑜}=1_{𝑜}\to \neg 1_{𝑜}\in 2_{𝑜}$$
8	3 7	mt2	$$⊢\neg 2_{𝑜}=1_{𝑜}$$
9	8	neir	$$⊢2_{𝑜}\ne 1_{𝑜}$$
10	2	unieqi	$$⊢\bigcup 2_{𝑜}=\bigcup \left\{\varnothing ,1_{𝑜}\right\}$$
11		0ex	$$⊢\varnothing \in \mathrm{V}$$
12		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
13	11 12	unipr	$$⊢\bigcup \left\{\varnothing ,1_{𝑜}\right\}=\varnothing \cup 1_{𝑜}$$
14		0un	$$⊢\varnothing \cup 1_{𝑜}=1_{𝑜}$$
15	10 13 14	3eqtri	$$⊢\bigcup 2_{𝑜}=1_{𝑜}$$
16	9 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}_{𝑜}$$