Theorem nsuceq0 6448

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 4284	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6446	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2850	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 248	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 202	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5261	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2849	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 261	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 155	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6441	. . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
11	10	eqeq1d 2763	. . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
12	9, 11	mtbird 328	. . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
13	5, 12	pm2.61i 184	. 2 ⊢ ¬ suc 𝐴 = ∅
14	13	neir 2959	1 ⊢ suc 𝐴 ≠ ∅

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  Vcvv 3451  ∅c0 4279  suc csuc 6364

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-un 3904  df-nul 4280  df-sn 4585  df-suc 6368

This theorem is used by:  0elsuc  7846  peano3OLD  7903  2on0  8491  1n0  8495  oelim2  8604  limenpsi  9171  ttrclselem2  9727  fseqdom  10105  dfac12lem2  10223  cfsuc  10335  cfpwsdom  10669  rankcf  10862  nosgnn0  28015  ltssolem1  28032  dfrdg2  36557  dfrdg4  36715  dfsucon  44523  ensucne0  44529  ensucne0OLD  44530