Theorem nsuceq0 6389

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 4282	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6387	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2826	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 245	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 198	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5256	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2825	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 258	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 154	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6382	. . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
11	10	eqeq1d 2739	. . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
12	9, 11	mtbird 325	. . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
13	5, 12	pm2.61i 182	. 2 ⊢ ¬ suc 𝐴 = ∅
14	13	neir 2944	1 ⊢ suc 𝐴 ≠ ∅

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2106   ≠ wne 2941  Vcvv 3442  ∅c0 4274  suc csuc 6309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-nul 5255

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-v 3444  df-dif 3905  df-un 3907  df-nul 4275  df-sn 4579  df-suc 6313

This theorem is referenced by:  0elsuc  7753  peano3  7811  2on0  8388  oelim2  8502  limenpsi  9022  enp1iOLD  9150  findcard2OLD  9154  ttrclselem2  9588  fseqdom  9888  dfac12lem2  10006  cfsuc  10119  cfpwsdom  10446  rankcf  10639  nosgnn0  26912  sltsolem1  26929  dfrdg2  34054  dfrdg4  34390  dfsucon  41502  ensucne0  41508  ensucne0OLD  41509