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

Theorem nsuceq0 4953
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 3784 . . . 4  |-  -.  A  e.  (/)
2 sucidg 4951 . . . . 5  |-  ( A  e.  _V  ->  A  e.  suc  A )
3 eleq2 2535 . . . . 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 4948 . . . . . . 7  |-  ( -.  A  e.  _V  ->  suc 
A  =  A )
76eqeq1d 2464 . . . . . 6  |-  ( -.  A  e.  _V  ->  ( suc  A  =  (/)  <->  A  =  (/) ) )
8 0ex 4572 . . . . . . 7  |-  (/)  e.  _V
9 eleq1 2534 . . . . . . 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 2662 1  |-  suc  A  =/=  (/)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1374    e. wcel 1762    =/= wne 2657   _Vcvv 3108   (/)c0 3780   suc csuc 4875
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 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-nul 4571
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-v 3110  df-dif 3474  df-un 3476  df-nul 3781  df-sn 4023  df-suc 4879
This theorem is referenced by:  0elsuc  6643  peano3  6694  2on0  7131  oelim2  7236  limenpsi  7684  enp1i  7746  findcard2  7751  fseqdom  8398  dfac12lem2  8515  cfsuc  8628  cfpwsdom  8950  rankcf  9146  dfrdg2  28793  nosgnn0  28983  sltsolem1  28993  dfrdg4  29165
  Copyright terms: Public domain W3C validator