dflim4

Description: An alternate definition of a limit ordinal. (Contributed by NM, 1-Feb-2005)

		Ref	Expression
	Assertion	dflim4	$⊢ Lim A \leftrightarrow (Ord A \land \emptyset \in A \land \forall x \in A suc x \in A)$

Step	Hyp	Ref	Expression
1		dflim2	$⊢ Lim A \leftrightarrow (Ord A \land \emptyset \in A \land A = ⋃ A)$
2		ordunisuc2	$⊢ Ord A \to (A = ⋃ A \leftrightarrow \forall x \in A suc x \in A)$
3	2	anbi2d	$⊢ Ord A \to ((\emptyset \in A \land A = ⋃ A) \leftrightarrow (\emptyset \in A \land \forall x \in A suc x \in A))$
4	3	pm5.32i	$⊢ (Ord A \land (\emptyset \in A \land A = ⋃ A)) \leftrightarrow (Ord A \land (\emptyset \in A \land \forall x \in A suc x \in 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 \emptyset \in A \land \forall x \in A suc x \in A) \leftrightarrow (Ord A \land (\emptyset \in A \land \forall x \in A suc x \in A))$
7	4 5 6	3bitr4i	$⊢ (Ord A \land \emptyset \in A \land A = ⋃ A) \leftrightarrow (Ord A \land \emptyset \in A \land \forall x \in A suc x \in A)$
8	1 7	bitri	$⊢ Lim A \leftrightarrow (Ord A \land \emptyset \in A \land \forall x \in A suc x \in A)$

Metamath Proof Explorer