Theorem nsuceq0 6454

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 4285	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6452	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2852	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 248	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 202	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5263	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2851	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 261	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 155	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6447	. . . . 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 2961	1 ⊢ suc 𝐴 ≠ ∅

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569   ∈ wcel 2146   ≠ wne 2958  Vcvv 3453  ∅c0 4280  suc csuc 6370

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-nul 5262

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3455  df-dif 4049  df-un 4153  df-nul 4281  df-sn 4588  df-suc 6374

This theorem is used by:  0elsuc  7853  peano3OLD  7910  2on0  8502  1n0  8506  oelim2  8615  limenpsi  9182  ttrclselem2  9737  fseqdom  10115  dfac12lem2  10233  cfsuc  10345  cfpwsdom  10679  rankcf  10872  nosgnn0  28027  ltssolem1  28044  jf1  35964  jf1o  35965  k39o  35971  jltalephlem  35979  dfrdg2  36684  dfrdg4  36842  dfsucon  44664  ensucne0  44670  ensucne0OLD  44671