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

Theorem nsuceq0 4575
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 3547 . . . 4  |-  -.  A  e.  (/)
2 sucidg 4573 . . . . 5  |-  ( A  e.  _V  ->  A  e.  suc  A )
3 eleq2 2427 . . . . 5  |-  ( suc 
A  =  (/)  ->  ( A  e.  suc  A  <->  A  e.  (/) ) )
42, 3syl5ibcom 211 . . . 4  |-  ( A  e.  _V  ->  ( suc  A  =  (/)  ->  A  e.  (/) ) )
51, 4mtoi 169 . . 3  |-  ( A  e.  _V  ->  -.  suc  A  =  (/) )
6 sucprc 4570 . . . . . . 7  |-  ( -.  A  e.  _V  ->  suc 
A  =  A )
76eqeq1d 2374 . . . . . 6  |-  ( -.  A  e.  _V  ->  ( suc  A  =  (/)  <->  A  =  (/) ) )
8 0ex 4252 . . . . . . 7  |-  (/)  e.  _V
9 eleq1 2426 . . . . . . 7  |-  ( A  =  (/)  ->  ( A  e.  _V  <->  (/)  e.  _V ) )
108, 9mpbiri 224 . . . . . 6  |-  ( A  =  (/)  ->  A  e. 
_V )
117, 10syl6bi 219 . . . . 5  |-  ( -.  A  e.  _V  ->  ( suc  A  =  (/)  ->  A  e.  _V )
)
1211con3d 125 . . . 4  |-  ( -.  A  e.  _V  ->  ( -.  A  e.  _V  ->  -.  suc  A  =  (/) ) )
1312pm2.43i 43 . . 3  |-  ( -.  A  e.  _V  ->  -. 
suc  A  =  (/) )
145, 13pm2.61i 156 . 2  |-  -.  suc  A  =  (/)
15 df-ne 2531 . 2  |-  ( suc 
A  =/=  (/)  <->  -.  suc  A  =  (/) )
1614, 15mpbir 200 1  |-  suc  A  =/=  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1647    e. wcel 1715    =/= wne 2529   _Vcvv 2873   (/)c0 3543   suc csuc 4497
This theorem is referenced by:  0elsuc  4729  peano3  4780  2on0  6630  oelim2  6735  limenpsi  7179  enp1i  7240  findcard2  7245  fseqdom  7800  dfac12lem2  7917  cfsuc  8030  cfpwsdom  8353  rankcf  8546  dfrdg2  24978  nosgnn0  25138  sltsolem1  25148  dfrdg4  25315
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-nul 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-v 2875  df-dif 3241  df-un 3243  df-nul 3544  df-sn 3735  df-suc 4501
  Copyright terms: Public domain W3C validator