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

Metamath Proof Explorer

Theorem 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 𝐴 → ( 𝐴 = ∪ 𝐴 ↔ ( 𝐴 = ∅ ∨ Lim 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 df-ne ⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
2 df-lim ⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) )
3 2 biimpri ⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) → Lim 𝐴 )
4 3 3exp ⊢ ( Ord 𝐴 → ( 𝐴 ≠ ∅ → ( 𝐴 = ∪ 𝐴 → Lim 𝐴 ) ) )
5 1 4 biimtrrid ⊢ ( Ord 𝐴 → ( ¬ 𝐴 = ∅ → ( 𝐴 = ∪ 𝐴 → Lim 𝐴 ) ) )
6 5 com23 ⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 → ( ¬ 𝐴 = ∅ → Lim 𝐴 ) ) )
7 6 imp ⊢ ( ( Ord 𝐴 ∧ 𝐴 = ∪ 𝐴 ) → ( ¬ 𝐴 = ∅ → Lim 𝐴 ) )
8 7 orrd ⊢ ( ( Ord 𝐴 ∧ 𝐴 = ∪ 𝐴 ) → ( 𝐴 = ∅ ∨ Lim 𝐴 ) )
9 8 ex ⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 → ( 𝐴 = ∅ ∨ Lim 𝐴 ) ) )
10 uni0 ⊢ ∪ ∅ = ∅
11 10 eqcomi ⊢ ∅ = ∪ ∅
12 id ⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
13 unieq ⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∪ ∅ )
14 11 12 13 3eqtr4a ⊢ ( 𝐴 = ∅ → 𝐴 = ∪ 𝐴 )
15 limuni ⊢ ( Lim 𝐴 → 𝐴 = ∪ 𝐴 )
16 14 15 jaoi ⊢ ( ( 𝐴 = ∅ ∨ Lim 𝐴 ) → 𝐴 = ∪ 𝐴 )
17 9 16 impbid1 ⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ↔ ( 𝐴 = ∅ ∨ Lim 𝐴 ) ) )