Theorem nsuceq0 6392

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 4289	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6390	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2817	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 245	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 199	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5246	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2816	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 258	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 154	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6385	. . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
11	10	eqeq1d 2731	. . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
12	9, 11	mtbird 325	. . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
13	5, 12	pm2.61i 182	. 2 ⊢ ¬ suc 𝐴 = ∅
14	13	neir 2928	1 ⊢ suc 𝐴 ≠ ∅

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  Vcvv 3436  ∅c0 4284  suc csuc 6309

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5245

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3438  df-dif 3906  df-un 3908  df-nul 4285  df-sn 4578  df-suc 6313

This theorem is referenced by:  0elsuc  7768  peano3  7824  2on0  8402  oelim2  8513  limenpsi  9069  ttrclselem2  9622  fseqdom  9920  dfac12lem2  10039  cfsuc  10151  cfpwsdom  10478  rankcf  10671  nosgnn0  27568  sltsolem1  27585  dfrdg2  35779  dfrdg4  35935  dfsucon  43506  ensucne0  43512  ensucne0OLD  43513