Metamath Proof Explorer

Theorem vdgfrgrgt2

Description: Any vertex in a friendship graph (with more than one vertex - then, actually, the graph must have at least three vertices, because otherwise, it would not be a friendship graph) has at least degree 2, see remark 3 in MertziosUnger p. 153 (after Proposition 1): "It follows that deg(v) >= 2 for every node v of a friendship graph". (Contributed by Alexander van der Vekens, 21-Dec-2017) (Revised by AV, 5-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 vdn1frgrv2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 vdgn0frgrv2 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 ) )
3 2 imp ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 )
4 1 vdgn1frgrv2 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 1 ) )
5 4 imp ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 1 )
6 1 vtxdgelxnn0 ⊢ ( 𝑁 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ∈ ℕ0* )
7 xnn0n0n1ge2b ⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ∈ ℕ0* → ( ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 1 ) ↔ 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ) )
8 6 7 syl ⊢ ( 𝑁 ∈ 𝑉 → ( ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 1 ) ↔ 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ) )
9 8 ad2antlr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 1 ) ↔ 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ) )
10 3 5 9 mpbi2and ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) )
11 10 ex ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ) )