Theorem nsuceq0 6363

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 4270	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6361	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2825	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 245	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 198	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5240	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2824	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 258	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 154	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6356	. . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
11	10	eqeq1d 2738	. . . 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 1539   ∈ wcel 2104   ≠ wne 2941  Vcvv 3437  ∅c0 4262  suc csuc 6283

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-nul 5239

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-v 3439  df-dif 3895  df-un 3897  df-nul 4263  df-sn 4566  df-suc 6287

This theorem is referenced by:  0elsuc  7714  peano3  7770  2on0  8344  oelim2  8457  limenpsi  8977  enp1i  9096  findcard2OLD  9100  ttrclselem2  9528  fseqdom  9828  dfac12lem2  9946  cfsuc  10059  cfpwsdom  10386  rankcf  10579  dfrdg2  33816  nosgnn0  33906  sltsolem1  33923  dfrdg4  34298  dfsucon  41168  ensucne0  41174  ensucne0OLD  41175