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

Theorem nsuceq0 4944
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 3771 . . . 4  |-  -.  A  e.  (/)
2 sucidg 4942 . . . . 5  |-  ( A  e.  _V  ->  A  e.  suc  A )
3 eleq2 2514 . . . . 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 4939 . . . . . . 7  |-  ( -.  A  e.  _V  ->  suc 
A  =  A )
76eqeq1d 2443 . . . . . 6  |-  ( -.  A  e.  _V  ->  ( suc  A  =  (/)  <->  A  =  (/) ) )
8 0ex 4563 . . . . . . 7  |-  (/)  e.  _V
9 eleq1 2513 . . . . . . 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 2641 1  |-  suc  A  =/=  (/)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1381    e. wcel 1802    =/= wne 2636   _Vcvv 3093   (/)c0 3767   suc csuc 4866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-nul 4562
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-v 3095  df-dif 3461  df-un 3463  df-nul 3768  df-sn 4011  df-suc 4870
This theorem is referenced by:  0elsuc  6651  peano3  6702  2on0  7137  oelim2  7242  limenpsi  7690  enp1i  7753  findcard2  7758  fseqdom  8405  dfac12lem2  8522  cfsuc  8635  cfpwsdom  8957  rankcf  9153  dfrdg2  29196  nosgnn0  29386  sltsolem1  29396  dfrdg4  29568
  Copyright terms: Public domain W3C validator