Theorem nsuceq0 6107

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 4182	. . . 4 ⊢ ¬ 𝐴 ∈ ∅
2		sucidg 6105	. . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		eleq2 2851	. . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅))
4	2, 3	syl5ibcom 237	. . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
5	1, 4	mtoi 191	. . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6		0ex 5066	. . . . . 6 ⊢ ∅ ∈ V
7		eleq1 2850	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
8	6, 7	mpbiri 250	. . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V)
9	8	con3i 152	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅)
10		sucprc 6102	. . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
11	10	eqeq1d 2777	. . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
12	9, 11	mtbird 317	. . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
13	5, 12	pm2.61i 177	. 2 ⊢ ¬ suc 𝐴 = ∅
14	13	neir 2967	1 ⊢ suc 𝐴 ≠ ∅

Syntax hints:  ¬ wn 3   = wceq 1507   ∈ wcel 2048   ≠ wne 2964  Vcvv 3412  ∅c0 4177  suc csuc 6029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2747  ax-nul 5065

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-v 3414  df-dif 3831  df-un 3833  df-nul 4178  df-sn 4440  df-suc 6033

This theorem is referenced by:  0elsuc  7364  peano3  7416  2on0  7911  oelim2  8018  limenpsi  8484  enp1i  8544  findcard2  8549  fseqdom  9242  dfac12lem2  9360  cfsuc  9473  cfpwsdom  9800  rankcf  9993  dfrdg2  32531  nosgnn0  32656  sltsolem1  32671  dfrdg4  32903