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 ⁡ A ≠ ∅

Proof

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