Metamath Proof Explorer

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 ⊢ V = Vtx ⁡ G
Assertion vdgn1frgrv3 ⊢ G ∈ FriendGraph ∧ 1 < V → ∀ v ∈ V VtxDeg ⁡ G ⁡ v ≠ 1

Proof

Step Hyp Ref Expression
1 vdn1frgrv2.v ⊢ V = Vtx ⁡ G
2 1 vdgn1frgrv2 ⊢ G ∈ FriendGraph ∧ v ∈ V → 1 < V → VtxDeg ⁡ G ⁡ v ≠ 1
3 2 impancom ⊢ G ∈ FriendGraph ∧ 1 < V → v ∈ V → VtxDeg ⁡ G ⁡ v ≠ 1
4 3 ralrimiv ⊢ G ∈ FriendGraph ∧ 1 < V → ∀ v ∈ V VtxDeg ⁡ G ⁡ v ≠ 1