| 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 =/= (/) |