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

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

Proof of Theorem nsuceq0
StepHypRef Expression
1 noel 4120 . . . 4 ¬ 𝐴 ∈ ∅
2 sucidg 6015 . . . . 5 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3 eleq2 2874 . . . . 5 (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴𝐴 ∈ ∅))
42, 3syl5ibcom 236 . . . 4 (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅))
51, 4mtoi 190 . . 3 (𝐴 ∈ V → ¬ suc 𝐴 = ∅)
6 0ex 4984 . . . . . 6 ∅ ∈ V
7 eleq1 2873 . . . . . 6 (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V))
86, 7mpbiri 249 . . . . 5 (𝐴 = ∅ → 𝐴 ∈ V)
98con3i 151 . . . 4 𝐴 ∈ V → ¬ 𝐴 = ∅)
10 sucprc 6012 . . . . 5 𝐴 ∈ V → suc 𝐴 = 𝐴)
1110eqeq1d 2808 . . . 4 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅))
129, 11mtbird 316 . . 3 𝐴 ∈ V → ¬ suc 𝐴 = ∅)
135, 12pm2.61i 176 . 2 ¬ suc 𝐴 = ∅
1413neir 2981 1 suc 𝐴 ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1637  wcel 2156  wne 2978  Vcvv 3391  c0 4116  suc csuc 5938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-nul 4983
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-v 3393  df-dif 3772  df-un 3774  df-nul 4117  df-sn 4371  df-suc 5942
This theorem is referenced by:  0elsuc  7261  peano3  7313  2on0  7802  oelim2  7908  limenpsi  8370  enp1i  8430  findcard2  8435  fseqdom  9128  dfac12lem2  9247  cfsuc  9360  cfpwsdom  9687  rankcf  9880  dfrdg2  32019  nosgnn0  32130  sltsolem1  32145  dfrdg4  32377
  Copyright terms: Public domain W3C validator