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

Metamath Proof Explorer

Theorem nlimsucg

Description: A successor is not a limit ordinal. (Contributed by NM, 25-Mar-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion nlimsucg ( 𝐴 ∈ 𝑉 → ¬ Lim suc 𝐴 )

Proof

Step Hyp Ref Expression
1 limord ⊢ ( Lim suc 𝐴 → Ord suc 𝐴 )
2 ordsuc ⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )
3 1 2 sylibr ⊢ ( Lim suc 𝐴 → Ord 𝐴 )
4 limuni ⊢ ( Lim suc 𝐴 → suc 𝐴 = ∪ suc 𝐴 )
5 ordunisuc ⊢ ( Ord 𝐴 → ∪ suc 𝐴 = 𝐴 )
6 5 eqeq2d ⊢ ( Ord 𝐴 → ( suc 𝐴 = ∪ suc 𝐴 ↔ suc 𝐴 = 𝐴 ) )
7 ordirr ⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )
8 eleq2 ⊢ ( suc 𝐴 = 𝐴 → ( 𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ 𝐴 ) )
9 8 notbid ⊢ ( suc 𝐴 = 𝐴 → ( ¬ 𝐴 ∈ suc 𝐴 ↔ ¬ 𝐴 ∈ 𝐴 ) )
10 7 9 syl5ibrcom ⊢ ( Ord 𝐴 → ( suc 𝐴 = 𝐴 → ¬ 𝐴 ∈ suc 𝐴 ) )
11 sucidg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴 )
12 11 con3i ⊢ ( ¬ 𝐴 ∈ suc 𝐴 → ¬ 𝐴 ∈ 𝑉 )
13 10 12 syl6 ⊢ ( Ord 𝐴 → ( suc 𝐴 = 𝐴 → ¬ 𝐴 ∈ 𝑉 ) )
14 6 13 sylbid ⊢ ( Ord 𝐴 → ( suc 𝐴 = ∪ suc 𝐴 → ¬ 𝐴 ∈ 𝑉 ) )
15 3 4 14 sylc ⊢ ( Lim suc 𝐴 → ¬ 𝐴 ∈ 𝑉 )
16 15 con2i ⊢ ( 𝐴 ∈ 𝑉 → ¬ Lim suc 𝐴 )