Metamath Proof Explorer

Theorem nsuceq0

Description: No successor is empty. (Contributed by NM, 3-Apr-1995)

Ref Expression
Assertion nsuceq0 
|- suc A =/= (/)

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. A e. (/)
2 sucidg 
 |-  ( A e. _V -> A e. suc A )
3 eleq2 
 |-  ( suc A = (/) -> ( A e. suc A <-> A e. (/) ) )
4 2 3 syl5ibcom 
 |-  ( A e. _V -> ( suc A = (/) -> A e. (/) ) )
5 1 4 mtoi 
 |-  ( A e. _V -> -. suc A = (/) )
6 0ex 
 |-  (/) e. _V
7 eleq1 
 |-  ( A = (/) -> ( A e. _V <-> (/) e. _V ) )
8 6 7 mpbiri 
 |-  ( A = (/) -> A e. _V )
9 8 con3i 
 |-  ( -. A e. _V -> -. A = (/) )
10 sucprc 
 |-  ( -. A e. _V -> suc A = A )
11 10 eqeq1d 
 |-  ( -. A e. _V -> ( suc A = (/) <-> A = (/) ) )
12 9 11 mtbird 
 |-  ( -. A e. _V -> -. suc A = (/) )
13 5 12 pm2.61i 
 |-  -. suc A = (/)
14 13 neir 
 |-  suc A =/= (/)