Theorem nsuceq0 6446

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 4329	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6444	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2820	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 244	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 198	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5306	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2819	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 257	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 154	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6439	. . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
11	10	eqeq1d 2732	. . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
12	9, 11	mtbird 324	. . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
13	5, 12	pm2.61i 182	. 2 ⊢ ¬ suc 𝐴 = ∅
14	13	neir 2941	1 ⊢ suc 𝐴 ≠ ∅

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2104   ≠ wne 2938  Vcvv 3472  ∅c0 4321  suc csuc 6365

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 2701  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-v 3474  df-dif 3950  df-un 3952  df-nul 4322  df-sn 4628  df-suc 6369

This theorem is referenced by:  0elsuc  7825  peano3  7884  2on0  8484  oelim2  8597  limenpsi  9154  enp1iOLD  9282  findcard2OLD  9286  ttrclselem2  9723  fseqdom  10023  dfac12lem2  10141  cfsuc  10254  cfpwsdom  10581  rankcf  10774  nosgnn0  27397  sltsolem1  27414  dfrdg2  35071  dfrdg4  35227  dfsucon  42576  ensucne0  42582  ensucne0OLD  42583