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

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion vdumgr0 ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = 0 )

Proof

Step Hyp Ref Expression
1 vdumgr0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 umgruhgr ⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
3 2 3ad2ant1 ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → 𝐺 ∈ UHGraph )
4 simp3 ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ♯ ‘ 𝑉 ) = 1 )
5 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
6 1 5 umgrislfupgr ⊢ ( 𝐺 ∈ UMGraph ↔ ( 𝐺 ∈ UPGraph ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
7 6 simprbi ⊢ ( 𝐺 ∈ UMGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
8 7 3ad2ant1 ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
9 3 4 8 3jca ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
10 simp2 ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → 𝑁 ∈ 𝑉 )
11 eqid ⊢ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
12 1 5 11 vtxdlfuhgr1v ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → ( 𝑁 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = 0 ) )
13 9 10 12 sylc ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = 0 )