This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )