Theorem nsuceq0 5805

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

Assertion

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

Proof of Theorem nsuceq0

Step	Hyp	Ref	Expression
1		noel 3919	. . . 4 |- -. A e. (/)
2		sucidg 5803	. . . . 5 |- ( A e. _V -> A e. suc A )
3		eleq2 2690	. . . . 5 |- ( suc A = (/) -> ( A e. suc A <-> A e. (/) ) )
4	2, 3	syl5ibcom 235	. . . 4 |- ( A e. _V -> ( suc A = (/) -> A e. (/) ) )
5	1, 4	mtoi 190	. . 3 |- ( A e. _V -> -. suc A = (/) )
6		0ex 4790	. . . . . 6 |- (/) e. _V
7		eleq1 2689	. . . . . 6 |- ( A = (/) -> ( A e. _V <-> (/) e. _V ) )
8	6, 7	mpbiri 248	. . . . 5 |- ( A = (/) -> A e. _V )
9	8	con3i 150	. . . 4 |- ( -. A e. _V -> -. A = (/) )
10		sucprc 5800	. . . . 5 |- ( -. A e. _V -> suc A = A )
11	10	eqeq1d 2624	. . . 4 |- ( -. A e. _V -> ( suc A = (/) <-> A = (/) ) )
12	9, 11	mtbird 315	. . 3 |- ( -. A e. _V -> -. suc A = (/) )
13	5, 12	pm2.61i 176	. 2 |- -. suc A = (/)
14	13	neir 2797	1 |- suc A =/= (/)

Syntax hints:   -. wn 3   = wceq 1483   e. wcel 1990   =/= wne 2794   _Vcvv 3200   (/)c0 3915   suc csuc 5725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-un 3579  df-nul 3916  df-sn 4178  df-suc 5729

This theorem is referenced by:  0elsuc  7035  peano3  7087  2on0  7569  oelim2  7675  limenpsi  8135  enp1i  8195  findcard2  8200  fseqdom  8849  dfac12lem2  8966  cfsuc  9079  cfpwsdom  9406  rankcf  9599  dfrdg2  31701  nosgnn0  31811  sltsolem1  31826  dfrdg4  32058