Metamath Proof Explorer

Theorem dflim6

Description: A limit ordinal is a non-zero ordinal which is not a succesor ordinal. Definition 1.11 of Schloeder p. 2. (Contributed by RP, 16-Jan-2025)

		Ref	Expression
	Assertion	dflim6	$⊢ Lim A \leftrightarrow (Ord A \land A \neq \emptyset \land \neg \exists b \in On A = suc b)$

Proof

Step	Hyp	Ref	Expression
1		ioran	$⊢ \neg (A = \emptyset \lor \exists b \in On A = suc b) \leftrightarrow (\neg A = \emptyset \land \neg \exists b \in On A = suc b)$
2		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
3	2	anbi1i	$⊢ (A \neq \emptyset \land \neg \exists b \in On A = suc b) \leftrightarrow (\neg A = \emptyset \land \neg \exists b \in On A = suc b)$
4	1 3	bitr4i	$⊢ \neg (A = \emptyset \lor \exists b \in On A = suc b) \leftrightarrow (A \neq \emptyset \land \neg \exists b \in On A = suc b)$
5	4	anbi2i	$⊢ (Ord A \land \neg (A = \emptyset \lor \exists b \in On A = suc b)) \leftrightarrow (Ord A \land (A \neq \emptyset \land \neg \exists b \in On A = suc b))$
6		dflim3	$⊢ Lim A \leftrightarrow (Ord A \land \neg (A = \emptyset \lor \exists b \in On A = suc b))$
7		3anass	$⊢ (Ord A \land A \neq \emptyset \land \neg \exists b \in On A = suc b) \leftrightarrow (Ord A \land (A \neq \emptyset \land \neg \exists b \in On A = suc b))$
8	5 6 7	3bitr4i	$⊢ Lim A \leftrightarrow (Ord A \land A \neq \emptyset \land \neg \exists b \in On A = suc b)$