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