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

Theorem nsuceq0 4625
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 3596 . . . 4  |-  -.  A  e.  (/)
2 sucidg 4623 . . . . 5  |-  ( A  e.  _V  ->  A  e.  suc  A )
3 eleq2 2469 . . . . 5  |-  ( suc 
A  =  (/)  ->  ( A  e.  suc  A  <->  A  e.  (/) ) )
42, 3syl5ibcom 212 . . . 4  |-  ( A  e.  _V  ->  ( suc  A  =  (/)  ->  A  e.  (/) ) )
51, 4mtoi 171 . . 3  |-  ( A  e.  _V  ->  -.  suc  A  =  (/) )
6 sucprc 4620 . . . . . . 7  |-  ( -.  A  e.  _V  ->  suc 
A  =  A )
76eqeq1d 2416 . . . . . 6  |-  ( -.  A  e.  _V  ->  ( suc  A  =  (/)  <->  A  =  (/) ) )
8 0ex 4303 . . . . . . 7  |-  (/)  e.  _V
9 eleq1 2468 . . . . . . 7  |-  ( A  =  (/)  ->  ( A  e.  _V  <->  (/)  e.  _V ) )
108, 9mpbiri 225 . . . . . 6  |-  ( A  =  (/)  ->  A  e. 
_V )
117, 10syl6bi 220 . . . . 5  |-  ( -.  A  e.  _V  ->  ( suc  A  =  (/)  ->  A  e.  _V )
)
1211con3d 127 . . . 4  |-  ( -.  A  e.  _V  ->  ( -.  A  e.  _V  ->  -.  suc  A  =  (/) ) )
1312pm2.43i 45 . . 3  |-  ( -.  A  e.  _V  ->  -. 
suc  A  =  (/) )
145, 13pm2.61i 158 . 2  |-  -.  suc  A  =  (/)
15 df-ne 2573 . 2  |-  ( suc 
A  =/=  (/)  <->  -.  suc  A  =  (/) )
1614, 15mpbir 201 1  |-  suc  A  =/=  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1649    e. wcel 1721    =/= wne 2571   _Vcvv 2920   (/)c0 3592   suc csuc 4547
This theorem is referenced by:  0elsuc  4778  peano3  4829  2on0  6696  oelim2  6801  limenpsi  7245  enp1i  7306  findcard2  7311  fseqdom  7867  dfac12lem2  7984  cfsuc  8097  cfpwsdom  8419  rankcf  8612  dfrdg2  25370  nosgnn0  25530  sltsolem1  25540  dfrdg4  25707
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-nul 4302
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-v 2922  df-dif 3287  df-un 3289  df-nul 3593  df-sn 3784  df-suc 4551
  Copyright terms: Public domain W3C validator