Theorem limelon

Description: A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004)

	Ref	Expression
Assertion	limelon	⊢ ( ( 𝐴 ∈ 𝐵 ∧ Lim 𝐴 ) → 𝐴 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		limord	⊢ ( Lim 𝐴 → Ord 𝐴 )
2		elong	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ On ↔ Ord 𝐴 ) )
3	1 2	imbitrrid	⊢ ( 𝐴 ∈ 𝐵 → ( Lim 𝐴 → 𝐴 ∈ On ) )
4	3	imp	⊢ ( ( 𝐴 ∈ 𝐵 ∧ Lim 𝐴 ) → 𝐴 ∈ On )