Metamath Proof Explorer

Theorem frgr2wwlkn0

Description: In a friendship graph, there is always a path/walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 12-May-2021)

Ref Expression
Hypothesis frgr2wwlkeu.v ⊢ V = Vtx ⁡ G
Assertion frgr2wwlkn0 ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A 2 WWalksNOn G B ≠ ∅

Proof

Step Hyp Ref Expression
1 frgr2wwlkeu.v ⊢ V = Vtx ⁡ G
2 1 frgr2wwlkeu ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → ∃! c ∈ V ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B
3 reurex ⊢ ∃! c ∈ V ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B → ∃ c ∈ V ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B
4 ne0i ⊢ ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B → A 2 WWalksNOn G B ≠ ∅
5 4 rexlimivw ⊢ ∃ c ∈ V ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B → A 2 WWalksNOn G B ≠ ∅
6 2 3 5 3syl ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A 2 WWalksNOn G B ≠ ∅