Theorem nsuceq0 6343

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 4269	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6341	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2828	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 244	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 198	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5234	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2827	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 257	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 154	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6338	. . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
11	10	eqeq1d 2741	. . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
12	9, 11	mtbird 324	. . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
13	5, 12	pm2.61i 182	. 2 ⊢ ¬ suc 𝐴 = ∅
14	13	neir 2947	1 ⊢ suc 𝐴 ≠ ∅

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2109   ≠ wne 2944  Vcvv 3430  ∅c0 4261  suc csuc 6265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-nul 5233

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-sn 4567  df-suc 6269

This theorem is referenced by:  0elsuc  7670  peano3  7725  2on0  8290  oelim2  8402  limenpsi  8904  enp1i  9013  findcard2OLD  9017  ttrclselem2  9445  fseqdom  9766  dfac12lem2  9884  cfsuc  9997  cfpwsdom  10324  rankcf  10517  dfrdg2  33750  nosgnn0  33840  sltsolem1  33857  dfrdg4  34232  dfsucon  41092  ensucne0  41098  ensucne0OLD  41099