Theorem vdgn1frgrv3

Description: Any vertex in a friendship graph does not have degree 1, see remark 2 in MertziosUnger p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 4-Sep-2018) (Revised by AV, 4-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		vdn1frgrv2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	vdgn1frgrv2	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑣 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ) )
3	2	impancom	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( 𝑣 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ) )
4	3	ralrimiv	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 )