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

Metamath Proof Explorer

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 𝐴 )