Description: In a finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 12-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | vtxdgfusgrf.v | |- V = ( Vtx ` G ) |
|
Assertion | vtxdgfusgr | |- ( G e. FinUSGraph -> A. v e. V ( ( VtxDeg ` G ) ` v ) e. NN0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtxdgfusgrf.v | |- V = ( Vtx ` G ) |
|
2 | 1 | vtxdgfusgrf | |- ( G e. FinUSGraph -> ( VtxDeg ` G ) : V --> NN0 ) |
3 | 2 | ffvelrnda | |- ( ( G e. FinUSGraph /\ v e. V ) -> ( ( VtxDeg ` G ) ` v ) e. NN0 ) |
4 | 3 | ralrimiva | |- ( G e. FinUSGraph -> A. v e. V ( ( VtxDeg ` G ) ` v ) e. NN0 ) |