This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem orduniorsuc

Description: An ordinal class is either its union or the successor of its union. If we adopt the view that zero is a limit ordinal, this means every ordinal class is either a limit or a successor. (Contributed by NM, 13-Sep-2003)

		Ref	Expression
	Assertion	orduniorsuc	$⊢ Ord A \to (A = ⋃ A \lor A = suc ⋃ A)$

Proof

Step	Hyp	Ref	Expression
1		orduniss	$⊢ Ord A \to ⋃ A \subseteq A$
2		orduni	$⊢ Ord A \to Ord ⋃ A$
3		ordelssne	$⊢ (Ord ⋃ A \land Ord A) \to (⋃ A \in A \leftrightarrow (⋃ A \subseteq A \land ⋃ A \neq A))$
4	2 3	mpancom	$⊢ Ord A \to (⋃ A \in A \leftrightarrow (⋃ A \subseteq A \land ⋃ A \neq A))$
5	4	biimprd	$⊢ Ord A \to ((⋃ A \subseteq A \land ⋃ A \neq A) \to ⋃ A \in A)$
6	1 5	mpand	$⊢ Ord A \to (⋃ A \neq A \to ⋃ A \in A)$
7		ordsucss	$⊢ Ord A \to (⋃ A \in A \to suc ⋃ A \subseteq A)$
8	6 7	syld	$⊢ Ord A \to (⋃ A \neq A \to suc ⋃ A \subseteq A)$
9		ordsucuni	$⊢ Ord A \to A \subseteq suc ⋃ A$
10	8 9	jctild	$⊢ Ord A \to (⋃ A \neq A \to (A \subseteq suc ⋃ A \land suc ⋃ A \subseteq A))$
11		df-ne	$⊢ A \neq ⋃ A \leftrightarrow \neg A = ⋃ A$
12		necom	$⊢ A \neq ⋃ A \leftrightarrow ⋃ A \neq A$
13	11 12	bitr3i	$⊢ \neg A = ⋃ A \leftrightarrow ⋃ A \neq A$
14		eqss	$⊢ A = suc ⋃ A \leftrightarrow (A \subseteq suc ⋃ A \land suc ⋃ A \subseteq A)$
15	10 13 14	3imtr4g	$⊢ Ord A \to (\neg A = ⋃ A \to A = suc ⋃ A)$
16	15	orrd	$⊢ Ord A \to (A = ⋃ A \lor A = suc ⋃ A)$