Metamath Proof Explorer

Theorem fusgrregdegfi

Description: In a nonempty finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018) (Revised by AV, 19-Dec-2020)

Ref Expression
Hypotheses isrusgr0.v 
|- V = ( Vtx ` G )
isrusgr0.d 
|- D = ( VtxDeg ` G )
Assertion fusgrregdegfi 
|- ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( D ` v ) = K -> K e. NN0 ) )

Proof

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 ) )