Theorem nsuceq0 6431

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 4290	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6429	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2851	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 247	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 201	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5257	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2850	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 260	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 154	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6424	. . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
11	10	eqeq1d 2764	. . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
12	9, 11	mtbird 327	. . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
13	5, 12	pm2.61i 183	. 2 ⊢ ¬ suc 𝐴 = ∅
14	13	neir 2960	1 ⊢ suc 𝐴 ≠ ∅

Syntax hints:  ¬ wn 3   = wceq 1560   ∈ wcel 2142   ≠ wne 2957  Vcvv 3454  ∅c0 4285  suc csuc 6348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5256

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3456  df-dif 3907  df-un 3909  df-nul 4286  df-sn 4583  df-suc 6352

This theorem is referenced by:  0elsuc  7815  peano3OLD  7872  2on0  8452  1n0  8456  oelim2  8565  limenpsi  9124  ttrclselem2  9681  fseqdom  9982  dfac12lem2  10101  cfsuc  10214  cfpwsdom  10542  rankcf  10735  nosgnn0  27722  ltssolem1  27739  dfrdg2  36143  dfrdg4  36301  dfsucon  44099  ensucne0  44105  ensucne0OLD  44106