Theorem nsuceq0 6437

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 4313	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6435	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2823	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 245	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 199	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5277	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2822	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 258	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 154	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6430	. . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
11	10	eqeq1d 2737	. . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
12	9, 11	mtbird 325	. . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
13	5, 12	pm2.61i 182	. 2 ⊢ ¬ suc 𝐴 = ∅
14	13	neir 2935	1 ⊢ suc 𝐴 ≠ ∅

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  Vcvv 3459  ∅c0 4308  suc csuc 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-un 3931  df-nul 4309  df-sn 4602  df-suc 6358

This theorem is referenced by:  0elsuc  7829  peano3  7887  2on0  8496  oelim2  8607  limenpsi  9166  enp1iOLD  9286  ttrclselem2  9740  fseqdom  10040  dfac12lem2  10159  cfsuc  10271  cfpwsdom  10598  rankcf  10791  nosgnn0  27622  sltsolem1  27639  dfrdg2  35813  dfrdg4  35969  dfsucon  43547  ensucne0  43553  ensucne0OLD  43554