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