MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nsuceq0 Structured version   Visualization version   GIF version

Theorem nsuceq0 6467
Description: No successor is empty. (Contributed by NM, 3-Apr-1995.)
Assertion
Ref Expression
nsuceq0 suc 𝐴 ≠ ∅

Proof of Theorem nsuceq0
StepHypRef Expression
1 noel 4338 . . . 4 ¬ 𝐴 ∈ ∅
2 sucidg 6465 . . . . 5 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3 eleq2 2830 . . . . 5 (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴𝐴 ∈ ∅))
42, 3syl5ibcom 245 . . . 4 (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
51, 4mtoi 199 . . 3 (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6 0ex 5307 . . . . . 6 ∅ ∈ V
7 eleq1 2829 . . . . . 6 (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
86, 7mpbiri 258 . . . . 5 (𝐴 = ∅ → 𝐴 ∈ V)
98con3i 154 . . . 4 𝐴 ∈ V → ¬ 𝐴 = ∅)
10 sucprc 6460 . . . . 5 𝐴 ∈ V → suc 𝐴 = 𝐴)
1110eqeq1d 2739 . . . 4 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
129, 11mtbird 325 . . 3 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
135, 12pm2.61i 182 . 2 ¬ suc 𝐴 = ∅
1413neir 2943 1 suc 𝐴 ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1540  wcel 2108  wne 2940  Vcvv 3480  c0 4333  suc csuc 6386
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334  df-sn 4627  df-suc 6390
This theorem is referenced by:  0elsuc  7855  peano3  7913  2on0  8522  oelim2  8633  limenpsi  9192  enp1iOLD  9314  ttrclselem2  9766  fseqdom  10066  dfac12lem2  10185  cfsuc  10297  cfpwsdom  10624  rankcf  10817  nosgnn0  27703  sltsolem1  27720  dfrdg2  35796  dfrdg4  35952  dfsucon  43536  ensucne0  43542  ensucne0OLD  43543
  Copyright terms: Public domain W3C validator