Step |
Hyp |
Ref |
Expression |
1 |
|
vtxdgf.v |
|- V = ( Vtx ` G ) |
2 |
1
|
eleq2i |
|- ( U e. V <-> U e. ( Vtx ` G ) ) |
3 |
|
fveq2 |
|- ( G = (/) -> ( Vtx ` G ) = ( Vtx ` (/) ) ) |
4 |
|
vtxval0 |
|- ( Vtx ` (/) ) = (/) |
5 |
3 4
|
eqtrdi |
|- ( G = (/) -> ( Vtx ` G ) = (/) ) |
6 |
5
|
eleq2d |
|- ( G = (/) -> ( U e. ( Vtx ` G ) <-> U e. (/) ) ) |
7 |
2 6
|
syl5bb |
|- ( G = (/) -> ( U e. V <-> U e. (/) ) ) |
8 |
|
noel |
|- -. U e. (/) |
9 |
8
|
pm2.21i |
|- ( U e. (/) -> ( ( VtxDeg ` G ) ` U ) = 0 ) |
10 |
7 9
|
syl6bi |
|- ( G = (/) -> ( U e. V -> ( ( VtxDeg ` G ) ` U ) = 0 ) ) |
11 |
10
|
imp |
|- ( ( G = (/) /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = 0 ) |