Metamath Proof Explorer


Theorem vtxdumgr0nedg

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 )