nlim1

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

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

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

Metamath Proof Explorer