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 )