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

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

Proof of Theorem nsuceq0
StepHypRef Expression
1 noel 4280 . . . 4 ¬ 𝐴 ∈ ∅
2 sucidg 6256 . . . . 5 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3 eleq2 2904 . . . . 5 (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴𝐴 ∈ ∅))
42, 3syl5ibcom 248 . . . 4 (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
51, 4mtoi 202 . . 3 (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6 0ex 5197 . . . . . 6 ∅ ∈ V
7 eleq1 2903 . . . . . 6 (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
86, 7mpbiri 261 . . . . 5 (𝐴 = ∅ → 𝐴 ∈ V)
98con3i 157 . . . 4 𝐴 ∈ V → ¬ 𝐴 = ∅)
10 sucprc 6253 . . . . 5 𝐴 ∈ V → suc 𝐴 = 𝐴)
1110eqeq1d 2826 . . . 4 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
129, 11mtbird 328 . . 3 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
135, 12pm2.61i 185 . 2 ¬ suc 𝐴 = ∅
1413neir 3017 1 suc 𝐴 ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1538  wcel 2115  wne 3014  Vcvv 3480  c0 4276  suc csuc 6180
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-11 2162  ax-12 2179  ax-ext 2796  ax-nul 5196
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-v 3482  df-dif 3922  df-un 3924  df-nul 4277  df-sn 4551  df-suc 6184
This theorem is referenced by:  0elsuc  7544  peano3  7597  2on0  8109  oelim2  8217  limenpsi  8689  enp1i  8750  findcard2  8755  fseqdom  9450  dfac12lem2  9568  cfsuc  9677  cfpwsdom  10004  rankcf  10197  dfrdg2  33100  nosgnn0  33225  sltsolem1  33240  dfrdg4  33472  dfsucon  40151  ensucne0  40157  ensucne0OLD  40158
  Copyright terms: Public domain W3C validator