Theorem nsuceq0

Description: No successor is empty. (Contributed by NM, 3-Apr-1995)

	Ref	Expression
Assertion	nsuceq0	⊢ suc 𝐴 ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ 𝐴 ∈ ∅
2		sucidg	⊢ ( 𝐴 ∈ V → 𝐴 ∈ suc 𝐴 )
3		eleq2	⊢ ( suc 𝐴 = ∅ → ( 𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅ ) )
4	2 3	syl5ibcom	⊢ ( 𝐴 ∈ V → ( suc 𝐴 = ∅ → 𝐴 ∈ ∅ ) )
5	1 4	mtoi	⊢ ( 𝐴 ∈ V → ¬ suc 𝐴 = ∅ )
6		0ex	⊢ ∅ ∈ V
7		eleq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ∈ V ↔ ∅ ∈ V ) )
8	6 7	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 ∈ V )
9	8	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐴 = ∅ )
10		sucprc	⊢ ( ¬ 𝐴 ∈ V → suc 𝐴 = 𝐴 )
11	10	eqeq1d	⊢ ( ¬ 𝐴 ∈ V → ( suc 𝐴 = ∅ ↔ 𝐴 = ∅ ) )
12	9 11	mtbird	⊢ ( ¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅ )
13	5 12	pm2.61i	⊢ ¬ suc 𝐴 = ∅
14	13	neir	⊢ suc 𝐴 ≠ ∅