Theorem nnlim

Description: A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995)

	Ref	Expression
Assertion	nnlim	⊢ ( 𝐴 ∈ ω → ¬ Lim 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nnord	⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
2		ordirr	⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )
3	1 2	syl	⊢ ( 𝐴 ∈ ω → ¬ 𝐴 ∈ 𝐴 )
4		elom	⊢ ( 𝐴 ∈ ω ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) ) )
5	4	simprbi	⊢ ( 𝐴 ∈ ω → ∀ 𝑥 ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) )
6		limeq	⊢ ( 𝑥 = 𝐴 → ( Lim 𝑥 ↔ Lim 𝐴 ) )
7		eleq2	⊢ ( 𝑥 = 𝐴 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐴 ) )
8	6 7	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) ↔ ( Lim 𝐴 → 𝐴 ∈ 𝐴 ) ) )
9	8	spcgv	⊢ ( 𝐴 ∈ ω → ( ∀ 𝑥 ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) → ( Lim 𝐴 → 𝐴 ∈ 𝐴 ) ) )
10	5 9	mpd	⊢ ( 𝐴 ∈ ω → ( Lim 𝐴 → 𝐴 ∈ 𝐴 ) )
11	3 10	mtod	⊢ ( 𝐴 ∈ ω → ¬ Lim 𝐴 )