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

Theorem nsuceq0 4795
Description: No successor is empty. (Contributed by NM, 3-Apr-1995.)
Assertion
Ref Expression
nsuceq0  |-  suc  A  =/=  (/)

Proof of Theorem nsuceq0
StepHypRef Expression
1 noel 3638 . . . 4  |-  -.  A  e.  (/)
2 sucidg 4793 . . . . 5  |-  ( A  e.  _V  ->  A  e.  suc  A )
3 eleq2 2502 . . . . 5  |-  ( suc 
A  =  (/)  ->  ( A  e.  suc  A  <->  A  e.  (/) ) )
42, 3syl5ibcom 220 . . . 4  |-  ( A  e.  _V  ->  ( suc  A  =  (/)  ->  A  e.  (/) ) )
51, 4mtoi 178 . . 3  |-  ( A  e.  _V  ->  -.  suc  A  =  (/) )
6 sucprc 4790 . . . . . . 7  |-  ( -.  A  e.  _V  ->  suc 
A  =  A )
76eqeq1d 2449 . . . . . 6  |-  ( -.  A  e.  _V  ->  ( suc  A  =  (/)  <->  A  =  (/) ) )
8 0ex 4419 . . . . . . 7  |-  (/)  e.  _V
9 eleq1 2501 . . . . . . 7  |-  ( A  =  (/)  ->  ( A  e.  _V  <->  (/)  e.  _V ) )
108, 9mpbiri 233 . . . . . 6  |-  ( A  =  (/)  ->  A  e. 
_V )
117, 10syl6bi 228 . . . . 5  |-  ( -.  A  e.  _V  ->  ( suc  A  =  (/)  ->  A  e.  _V )
)
1211con3d 133 . . . 4  |-  ( -.  A  e.  _V  ->  ( -.  A  e.  _V  ->  -.  suc  A  =  (/) ) )
1312pm2.43i 47 . . 3  |-  ( -.  A  e.  _V  ->  -. 
suc  A  =  (/) )
145, 13pm2.61i 164 . 2  |-  -.  suc  A  =  (/)
1514neir 2609 1  |-  suc  A  =/=  (/)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1364    e. wcel 1761    =/= wne 2604   _Vcvv 2970   (/)c0 3634   suc csuc 4717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-nul 4418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-v 2972  df-dif 3328  df-un 3330  df-nul 3635  df-sn 3875  df-suc 4721
This theorem is referenced by:  0elsuc  6445  peano3  6496  2on0  6925  oelim2  7030  limenpsi  7482  enp1i  7543  findcard2  7548  fseqdom  8192  dfac12lem2  8309  cfsuc  8422  cfpwsdom  8744  rankcf  8940  dfrdg2  27522  nosgnn0  27712  sltsolem1  27722  dfrdg4  27894
  Copyright terms: Public domain W3C validator