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

Theorem nsuceq0 4472
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 3459 . . . 4  |-  -.  A  e.  (/)
2 sucidg 4470 . . . . 5  |-  ( A  e.  _V  ->  A  e.  suc  A )
3 eleq2 2344 . . . . 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 4467 . . . . . . 7  |-  ( -.  A  e.  _V  ->  suc 
A  =  A )
76eqeq1d 2291 . . . . . 6  |-  ( -.  A  e.  _V  ->  ( suc  A  =  (/)  <->  A  =  (/) ) )
8 0ex 4150 . . . . . . 7  |-  (/)  e.  _V
9 eleq1 2343 . . . . . . 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 2448 . 2  |-  ( suc 
A  =/=  (/)  <->  -.  suc  A  =  (/) )
1614, 15mpbir 200 1  |-  suc  A  =/=  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1623    e. wcel 1684    =/= wne 2446   _Vcvv 2788   (/)c0 3455   suc csuc 4394
This theorem is referenced by:  0elsuc  4626  peano3  4677  2on0  6488  oelim2  6593  limenpsi  7036  enp1i  7093  findcard2  7098  fseqdom  7653  dfac12lem2  7770  cfsuc  7883  cfpwsdom  8206  rankcf  8399  dfrdg2  24152  nosgnn0  24312  sltsolem1  24322  dfrdg4  24488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-un 3157  df-nul 3456  df-sn 3646  df-suc 4398
  Copyright terms: Public domain W3C validator