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 𝐴 → ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		orduniss	⊢ ( Ord 𝐴 → ∪ 𝐴 ⊆ 𝐴 )
2		orduni	⊢ ( Ord 𝐴 → Ord ∪ 𝐴 )
3		ordelssne	⊢ ( ( Ord ∪ 𝐴 ∧ Ord 𝐴 ) → ( ∪ 𝐴 ∈ 𝐴 ↔ ( ∪ 𝐴 ⊆ 𝐴 ∧ ∪ 𝐴 ≠ 𝐴 ) ) )
4	2 3	mpancom	⊢ ( Ord 𝐴 → ( ∪ 𝐴 ∈ 𝐴 ↔ ( ∪ 𝐴 ⊆ 𝐴 ∧ ∪ 𝐴 ≠ 𝐴 ) ) )
5	4	biimprd	⊢ ( Ord 𝐴 → ( ( ∪ 𝐴 ⊆ 𝐴 ∧ ∪ 𝐴 ≠ 𝐴 ) → ∪ 𝐴 ∈ 𝐴 ) )
6	1 5	mpand	⊢ ( Ord 𝐴 → ( ∪ 𝐴 ≠ 𝐴 → ∪ 𝐴 ∈ 𝐴 ) )
7		ordsucss	⊢ ( Ord 𝐴 → ( ∪ 𝐴 ∈ 𝐴 → suc ∪ 𝐴 ⊆ 𝐴 ) )
8	6 7	syld	⊢ ( Ord 𝐴 → ( ∪ 𝐴 ≠ 𝐴 → suc ∪ 𝐴 ⊆ 𝐴 ) )
9		ordsucuni	⊢ ( Ord 𝐴 → 𝐴 ⊆ suc ∪ 𝐴 )
10	8 9	jctild	⊢ ( Ord 𝐴 → ( ∪ 𝐴 ≠ 𝐴 → ( 𝐴 ⊆ suc ∪ 𝐴 ∧ suc ∪ 𝐴 ⊆ 𝐴 ) ) )
11		df-ne	⊢ ( 𝐴 ≠ ∪ 𝐴 ↔ ¬ 𝐴 = ∪ 𝐴 )
12		necom	⊢ ( 𝐴 ≠ ∪ 𝐴 ↔ ∪ 𝐴 ≠ 𝐴 )
13	11 12	bitr3i	⊢ ( ¬ 𝐴 = ∪ 𝐴 ↔ ∪ 𝐴 ≠ 𝐴 )
14		eqss	⊢ ( 𝐴 = suc ∪ 𝐴 ↔ ( 𝐴 ⊆ suc ∪ 𝐴 ∧ suc ∪ 𝐴 ⊆ 𝐴 ) )
15	10 13 14	3imtr4g	⊢ ( Ord 𝐴 → ( ¬ 𝐴 = ∪ 𝐴 → 𝐴 = suc ∪ 𝐴 ) )
16	15	orrd	⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 ) )