Theorem nsuceq0 6450

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

Assertion

Ref	Expression
nsuceq0	⊢ suc 𝐴 ≠ ∅

Proof of Theorem nsuceq0

Step	Hyp	Ref	Expression
1		noel 4291	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6448	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2854	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 248	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 202	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5272	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2853	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 261	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 155	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6443	. . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
11	10	eqeq1d 2767	. . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
12	9, 11	mtbird 328	. . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
13	5, 12	pm2.61i 184	. 2 ⊢ ¬ suc 𝐴 = ∅
14	13	neir 2963	1 ⊢ suc 𝐴 ≠ ∅

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  Vcvv 3457  ∅c0 4286  suc csuc 6366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-v 3459  df-dif 3909  df-un 3911  df-nul 4287  df-sn 4592  df-suc 6370

This theorem is used by:  0elsuc  7837  peano3OLD  7894  2on0  8474  1n0  8478  oelim2  8587  limenpsi  9147  ttrclselem2  9702  fseqdom  10026  dfac12lem2  10144  cfsuc  10256  cfpwsdom  10586  rankcf  10779  nosgnn0  27875  ltssolem1  27892  dfrdg2  36324  dfrdg4  36482  dfsucon  44309  ensucne0  44315  ensucne0OLD  44316