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

Metamath Proof Explorer

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 𝐴 ≠ ∅