Metamath Proof Explorer

Theorem dflim3

Description: An alternate definition of a limit ordinal, which is any ordinal that is neither zero nor a successor. (Contributed by NM, 1-Nov-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	dflim3	$⊢ Lim A \leftrightarrow (Ord A \land \neg (A = \emptyset \lor \exists x \in On A = suc x))$

Proof

Step	Hyp	Ref	Expression
1		df-lim	$⊢ Lim A \leftrightarrow (Ord A \land A \neq \emptyset \land A = ⋃ A)$
2		3anass	$⊢ (Ord A \land A \neq \emptyset \land A = ⋃ A) \leftrightarrow (Ord A \land (A \neq \emptyset \land A = ⋃ A))$
3		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
4	3	a1i	$⊢ Ord A \to (A \neq \emptyset \leftrightarrow \neg A = \emptyset)$
5		orduninsuc	$⊢ Ord A \to (A = ⋃ A \leftrightarrow \neg \exists x \in On A = suc x)$
6	4 5	anbi12d	$⊢ Ord A \to ((A \neq \emptyset \land A = ⋃ A) \leftrightarrow (\neg A = \emptyset \land \neg \exists x \in On A = suc x))$
7		ioran	$⊢ \neg (A = \emptyset \lor \exists x \in On A = suc x) \leftrightarrow (\neg A = \emptyset \land \neg \exists x \in On A = suc x)$
8	6 7	bitr4di	$⊢ Ord A \to ((A \neq \emptyset \land A = ⋃ A) \leftrightarrow \neg (A = \emptyset \lor \exists x \in On A = suc x))$
9	8	pm5.32i	$⊢ (Ord A \land (A \neq \emptyset \land A = ⋃ A)) \leftrightarrow (Ord A \land \neg (A = \emptyset \lor \exists x \in On A = suc x))$
10	1 2 9	3bitri	$⊢ Lim A \leftrightarrow (Ord A \land \neg (A = \emptyset \lor \exists x \in On A = suc x))$