dflim2

Description: An alternate definition of a limit ordinal. (Contributed by NM, 4-Nov-2004)

		Ref	Expression
	Assertion	dflim2	$⊢ Lim A \leftrightarrow (Ord A \land \emptyset \in A \land A = ⋃ A)$

Step	Hyp	Ref	Expression
1		df-lim	$⊢ Lim A \leftrightarrow (Ord A \land A \neq \emptyset \land A = ⋃ A)$
2		ord0eln0	$⊢ Ord A \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
3	2	anbi1d	$⊢ Ord A \to ((\emptyset \in A \land A = ⋃ A) \leftrightarrow (A \neq \emptyset \land A = ⋃ A))$
4	3	pm5.32i	$⊢ (Ord A \land (\emptyset \in A \land A = ⋃ A)) \leftrightarrow (Ord A \land (A \neq \emptyset \land A = ⋃ A))$
5		3anass	$⊢ (Ord A \land \emptyset \in A \land A = ⋃ A) \leftrightarrow (Ord A \land (\emptyset \in A \land A = ⋃ A))$
6		3anass	$⊢ (Ord A \land A \neq \emptyset \land A = ⋃ A) \leftrightarrow (Ord A \land (A \neq \emptyset \land A = ⋃ A))$
7	4 5 6	3bitr4i	$⊢ (Ord A \land \emptyset \in A \land A = ⋃ A) \leftrightarrow (Ord A \land A \neq \emptyset \land A = ⋃ A)$
8	1 7	bitr4i	$⊢ Lim A \leftrightarrow (Ord A \land \emptyset \in A \land A = ⋃ A)$

Metamath Proof Explorer