2ellim

Description: A limit ordinal contains 2. (Contributed by BTernaryTau, 1-Dec-2024)

		Ref	Expression
	Assertion	2ellim	$⊢ Lim A \to 2_{𝑜} \in A$

Step	Hyp	Ref	Expression
1		nlim0	$⊢ \neg Lim \emptyset$
2		limeq	$⊢ A = \emptyset \to (Lim A \leftrightarrow Lim \emptyset)$
3	1 2	mtbiri	$⊢ A = \emptyset \to \neg Lim A$
4	3	necon2ai	$⊢ Lim A \to A \neq \emptyset$
5		nlim1	$⊢ \neg Lim 1_{𝑜}$
6		limeq	$⊢ A = 1_{𝑜} \to (Lim A \leftrightarrow Lim 1_{𝑜})$
7	5 6	mtbiri	$⊢ A = 1_{𝑜} \to \neg Lim A$
8	7	necon2ai	$⊢ Lim A \to A \neq 1_{𝑜}$
9		nlim2	$⊢ \neg Lim 2_{𝑜}$
10		limeq	$⊢ A = 2_{𝑜} \to (Lim A \leftrightarrow Lim 2_{𝑜})$
11	9 10	mtbiri	$⊢ A = 2_{𝑜} \to \neg Lim A$
12	11	necon2ai	$⊢ Lim A \to A \neq 2_{𝑜}$
13		limord	$⊢ Lim A \to Ord A$
14		ord2eln012	$⊢ Ord A \to (2_{𝑜} \in A \leftrightarrow (A \neq \emptyset \land A \neq 1_{𝑜} \land A \neq 2_{𝑜}))$
15	13 14	syl	$⊢ Lim A \to (2_{𝑜} \in A \leftrightarrow (A \neq \emptyset \land A \neq 1_{𝑜} \land A \neq 2_{𝑜}))$
16	4 8 12 15	mpbir3and	$⊢ Lim A \to 2_{𝑜} \in A$

Metamath Proof Explorer