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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vtxdushgrfvedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	vtxdushgrfvedg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion	vtxdumgr0nedg	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑈 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑈 ) = 0 ) → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		vtxdushgrfvedg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		vtxdushgrfvedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		vtxdushgrfvedg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4		umgruhgr	⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
5	1 2 3	vtxduhgr0nedg	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑈 ) = 0 ) → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 )
6	4 5	syl3an1	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑈 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑈 ) = 0 ) → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 )