Theorem 0ellim

Description: A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994)

	Ref	Expression
Assertion	0ellim	⊢ ( Lim 𝐴 → ∅ ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nlim0	⊢ ¬ Lim ∅
2		limeq	⊢ ( 𝐴 = ∅ → ( Lim 𝐴 ↔ Lim ∅ ) )
3	1 2	mtbiri	⊢ ( 𝐴 = ∅ → ¬ Lim 𝐴 )
4	3	necon2ai	⊢ ( Lim 𝐴 → 𝐴 ≠ ∅ )
5		limord	⊢ ( Lim 𝐴 → Ord 𝐴 )
6		ord0eln0	⊢ ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
7	5 6	syl	⊢ ( Lim 𝐴 → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
8	4 7	mpbird	⊢ ( Lim 𝐴 → ∅ ∈ 𝐴 )