unizlim

Description: An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003)

		Ref	Expression
	Assertion	unizlim	$⊢ Ord A \to (A = ⋃ A \leftrightarrow (A = \emptyset \lor Lim A))$

Step	Hyp	Ref	Expression
1		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
2		df-lim	$⊢ Lim A \leftrightarrow (Ord A \land A \neq \emptyset \land A = ⋃ A)$
3	2	biimpri	$⊢ (Ord A \land A \neq \emptyset \land A = ⋃ A) \to Lim A$
4	3	3exp	$⊢ Ord A \to (A \neq \emptyset \to (A = ⋃ A \to Lim A))$
5	1 4	biimtrrid	$⊢ Ord A \to (\neg A = \emptyset \to (A = ⋃ A \to Lim A))$
6	5	com23	$⊢ Ord A \to (A = ⋃ A \to (\neg A = \emptyset \to Lim A))$
7	6	imp	$⊢ (Ord A \land A = ⋃ A) \to (\neg A = \emptyset \to Lim A)$
8	7	orrd	$⊢ (Ord A \land A = ⋃ A) \to (A = \emptyset \lor Lim A)$
9	8	ex	$⊢ Ord A \to (A = ⋃ A \to (A = \emptyset \lor Lim A))$
10		uni0	$⊢ ⋃ \emptyset = \emptyset$
11	10	eqcomi	$⊢ \emptyset = ⋃ \emptyset$
12		id	$⊢ A = \emptyset \to A = \emptyset$
13		unieq	$⊢ A = \emptyset \to ⋃ A = ⋃ \emptyset$
14	11 12 13	3eqtr4a	$⊢ A = \emptyset \to A = ⋃ A$
15		limuni	$⊢ Lim A \to A = ⋃ A$
16	14 15	jaoi	$⊢ (A = \emptyset \lor Lim A) \to A = ⋃ A$
17	9 16	impbid1	$⊢ Ord A \to (A = ⋃ A \leftrightarrow (A = \emptyset \lor Lim A))$

Metamath Proof Explorer