Theorem nsuceq0 6474

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 4286	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6472	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2853	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 248	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 202	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5267	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2852	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 261	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 155	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6467	. . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
11	10	eqeq1d 2765	. . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
12	9, 11	mtbird 328	. . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
13	5, 12	pm2.61i 184	. 2 ⊢ ¬ suc 𝐴 = ∅
14	13	neir 2962	1 ⊢ suc 𝐴 ≠ ∅

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  Vcvv 3454  ∅c0 4281  suc csuc 6390

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5266

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-suc 6394

This theorem is used by:  0elsuc  7880  peano3OLD  7937  2on0  8529  1n0  8533  oelim2  8642  limenpsi  9209  ttrclselem2  9764  fseqdom  10144  dfac12lem2  10262  cfsuc  10374  cfpwsdom  10708  rankcf  10901  nosgnn0  28072  ltssolem1  28089  suceldifsn0  35832  jf1  36051  jf1o  36052  k39o  36058  jltalephlem  36066  dfrdg2  36772  dfrdg4  36930  dfsucon  44785  ensucne0  44791  ensucne0OLD  44792