1ellim

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

		Ref	Expression
	Assertion	1ellim	$⊢ Lim A \to 1_{𝑜} \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		limord	$⊢ Lim A \to Ord A$
10		ord1eln01	$⊢ Ord A \to (1_{𝑜} \in A \leftrightarrow (A \neq \emptyset \land A \neq 1_{𝑜}))$
11	9 10	syl	$⊢ Lim A \to (1_{𝑜} \in A \leftrightarrow (A \neq \emptyset \land A \neq 1_{𝑜}))$
12	4 8 11	mpbir2and	$⊢ Lim A \to 1_{𝑜} \in A$

Metamath Proof Explorer