Metamath Proof Explorer

Theorem vdumgr0

Description: A vertex in a multigraph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 2-Apr-2021)

Ref Expression
Hypothesis vdumgr0.v ⊢ V = Vtx ⁡ G
Assertion vdumgr0 ⊢ G ∈ UMGraph ∧ N ∈ V ∧ V = 1 → VtxDeg ⁡ G ⁡ N = 0

Proof

Step Hyp Ref Expression
1 vdumgr0.v ⊢ V = Vtx ⁡ G
2 umgruhgr ⊢ G ∈ UMGraph → G ∈ UHGraph
3 2 3ad2ant1 ⊢ G ∈ UMGraph ∧ N ∈ V ∧ V = 1 → G ∈ UHGraph
4 simp3 ⊢ G ∈ UMGraph ∧ N ∈ V ∧ V = 1 → V = 1
5 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
6 1 5 umgrislfupgr ⊢ G ∈ UMGraph ↔ G ∈ UPGraph ∧ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 V | 2 ≤ x
7 6 simprbi ⊢ G ∈ UMGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 V | 2 ≤ x
8 7 3ad2ant1 ⊢ G ∈ UMGraph ∧ N ∈ V ∧ V = 1 → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 V | 2 ≤ x
9 3 4 8 3jca ⊢ G ∈ UMGraph ∧ N ∈ V ∧ V = 1 → G ∈ UHGraph ∧ V = 1 ∧ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 V | 2 ≤ x
10 simp2 ⊢ G ∈ UMGraph ∧ N ∈ V ∧ V = 1 → N ∈ V
11 eqid ⊢ x ∈ 𝒫 V | 2 ≤ x = x ∈ 𝒫 V | 2 ≤ x
12 1 5 11 vtxdlfuhgr1v ⊢ G ∈ UHGraph ∧ V = 1 ∧ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 V | 2 ≤ x → N ∈ V → VtxDeg ⁡ G ⁡ N = 0
13 9 10 12 sylc ⊢ G ∈ UMGraph ∧ N ∈ V ∧ V = 1 → VtxDeg ⁡ G ⁡ N = 0