Theorem vdgn0frgrv2

Description: A vertex in a friendship graph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017) (Revised by AV, 4-Apr-2021)

	Ref	Expression
Hypothesis	vdn1frgrv2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	vdgn0frgrv2	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		vdn1frgrv2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frgrconngr	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ ConnGraph )
3		frgrusgr	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
4		usgrumgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
5	3 4	syl	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ UMGraph )
6	1	vdn0conngrumgrv2	⊢ ( ( ( 𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph ) ∧ ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 )
7	6	ex	⊢ ( ( 𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph ) → ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 ) )
8	2 5 7	syl2anc	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 ) )
9	8	expdimp	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 ) )