Theorem nlim1

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

	Ref	Expression
Assertion	nlim1	$$⊢\neg \mathrm{Lim}{1}_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		1n0	$$⊢1_{𝑜}\ne \varnothing$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	2	unisn	$$⊢\bigcup \left\{\varnothing \right\}=\varnothing$$
4	1 3	neeqtrri	$$⊢1_{𝑜}\ne \bigcup \left\{\varnothing \right\}$$
5		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
6	5	unieqi	$$⊢\bigcup 1_{𝑜}=\bigcup \left\{\varnothing \right\}$$
7	4 6	neeqtrri	$$⊢1_{𝑜}\ne \bigcup 1_{𝑜}$$
8	7	neii	$$⊢\neg 1_{𝑜}=\bigcup 1_{𝑜}$$
9		simp3	$$⊢\left(\mathrm{Ord}{1}_{𝑜}\wedge 1_{𝑜}\ne \varnothing \wedge 1_{𝑜}=\bigcup 1_{𝑜}\right)\to 1_{𝑜}=\bigcup 1_{𝑜}$$
10	8 9	mto	$$⊢\neg \left(\mathrm{Ord}{1}_{𝑜}\wedge 1_{𝑜}\ne \varnothing \wedge 1_{𝑜}=\bigcup 1_{𝑜}\right)$$
11		df-lim	$$⊢\mathrm{Lim}{1}_{𝑜}\leftrightarrow \left(\mathrm{Ord}{1}_{𝑜}\wedge 1_{𝑜}\ne \varnothing \wedge 1_{𝑜}=\bigcup 1_{𝑜}\right)$$
12	10 11	mtbir	$$⊢\neg \mathrm{Lim}{1}_{𝑜}$$