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	syl5bir	⊢ ( 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 𝐴 ) ) )