Step |
Hyp |
Ref |
Expression |
1 |
|
isrusgr0.v |
|- V = ( Vtx ` G ) |
2 |
|
isrusgr0.d |
|- D = ( VtxDeg ` G ) |
3 |
1
|
vtxdgfusgr |
|- ( G e. FinUSGraph -> A. v e. V ( ( VtxDeg ` G ) ` v ) e. NN0 ) |
4 |
|
r19.26 |
|- ( A. v e. V ( ( ( VtxDeg ` G ) ` v ) e. NN0 /\ ( D ` v ) = K ) <-> ( A. v e. V ( ( VtxDeg ` G ) ` v ) e. NN0 /\ A. v e. V ( D ` v ) = K ) ) |
5 |
2
|
fveq1i |
|- ( D ` v ) = ( ( VtxDeg ` G ) ` v ) |
6 |
5
|
eqeq1i |
|- ( ( D ` v ) = K <-> ( ( VtxDeg ` G ) ` v ) = K ) |
7 |
|
eleq1 |
|- ( ( ( VtxDeg ` G ) ` v ) = K -> ( ( ( VtxDeg ` G ) ` v ) e. NN0 <-> K e. NN0 ) ) |
8 |
6 7
|
sylbi |
|- ( ( D ` v ) = K -> ( ( ( VtxDeg ` G ) ` v ) e. NN0 <-> K e. NN0 ) ) |
9 |
8
|
biimpac |
|- ( ( ( ( VtxDeg ` G ) ` v ) e. NN0 /\ ( D ` v ) = K ) -> K e. NN0 ) |
10 |
9
|
ralimi |
|- ( A. v e. V ( ( ( VtxDeg ` G ) ` v ) e. NN0 /\ ( D ` v ) = K ) -> A. v e. V K e. NN0 ) |
11 |
|
rspn0 |
|- ( V =/= (/) -> ( A. v e. V K e. NN0 -> K e. NN0 ) ) |
12 |
10 11
|
syl5com |
|- ( A. v e. V ( ( ( VtxDeg ` G ) ` v ) e. NN0 /\ ( D ` v ) = K ) -> ( V =/= (/) -> K e. NN0 ) ) |
13 |
4 12
|
sylbir |
|- ( ( A. v e. V ( ( VtxDeg ` G ) ` v ) e. NN0 /\ A. v e. V ( D ` v ) = K ) -> ( V =/= (/) -> K e. NN0 ) ) |
14 |
13
|
ex |
|- ( A. v e. V ( ( VtxDeg ` G ) ` v ) e. NN0 -> ( A. v e. V ( D ` v ) = K -> ( V =/= (/) -> K e. NN0 ) ) ) |
15 |
14
|
com23 |
|- ( A. v e. V ( ( VtxDeg ` G ) ` v ) e. NN0 -> ( V =/= (/) -> ( A. v e. V ( D ` v ) = K -> K e. NN0 ) ) ) |
16 |
3 15
|
syl |
|- ( G e. FinUSGraph -> ( V =/= (/) -> ( A. v e. V ( D ` v ) = K -> K e. NN0 ) ) ) |
17 |
16
|
imp |
|- ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( D ` v ) = K -> K e. NN0 ) ) |