nlim2

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

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

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

Metamath Proof Explorer