Database
GRAPH THEORY
Undirected graphs
Vertex degree
vtxdumgr0nedg
Metamath Proof Explorer
Description: If a vertex in a multigraph has degree 0, the vertex is not adjacent to
another vertex via an edge. (Contributed by Alexander van der Vekens , 8-Dec-2017) (Revised by AV , 12-Dec-2020) (Proof shortened by AV , 15-Dec-2020)
Ref
Expression
Hypotheses
vtxdushgrfvedg.v
|- V = ( Vtx ` G )
vtxdushgrfvedg.e
|- E = ( Edg ` G )
vtxdushgrfvedg.d
|- D = ( VtxDeg ` G )
Assertion
vtxdumgr0nedg
|- ( ( G e. UMGraph /\ U e. V /\ ( D ` U ) = 0 ) -> -. E. v e. V { U , v } e. E )
Proof
Step
Hyp
Ref
Expression
1
vtxdushgrfvedg.v
|- V = ( Vtx ` G )
2
vtxdushgrfvedg.e
|- E = ( Edg ` G )
3
vtxdushgrfvedg.d
|- D = ( VtxDeg ` G )
4
umgruhgr
|- ( G e. UMGraph -> G e. UHGraph )
5
1 2 3
vtxduhgr0nedg
|- ( ( G e. UHGraph /\ U e. V /\ ( D ` U ) = 0 ) -> -. E. v e. V { U , v } e. E )
6
4 5
syl3an1
|- ( ( G e. UMGraph /\ U e. V /\ ( D ` U ) = 0 ) -> -. E. v e. V { U , v } e. E )