Description: The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017) (Revised by AV, 10-Dec-2020) (Revised by AV, 22-Mar-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | vtxdgf.v | |- V = ( Vtx ` G ) |
|
| Assertion | vtxdgelxnn0 | |- ( X e. V -> ( ( VtxDeg ` G ) ` X ) e. NN0* ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vtxdgf.v | |- V = ( Vtx ` G ) |
|
| 2 | 1 | 1vgrex | |- ( X e. V -> G e. _V ) |
| 3 | 1 | vtxdgf | |- ( G e. _V -> ( VtxDeg ` G ) : V --> NN0* ) |
| 4 | 3 | ffvelrnda | |- ( ( G e. _V /\ X e. V ) -> ( ( VtxDeg ` G ) ` X ) e. NN0* ) |
| 5 | 2 4 | mpancom | |- ( X e. V -> ( ( VtxDeg ` G ) ` X ) e. NN0* ) |