Metamath Proof Explorer

Theorem frgr2wwlkeu

Description: For two different vertices in a friendship graph, there is exactly one third vertex being the middle vertex of a (simple) path/walk of length 2 between the two vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 12-May-2021) (Proof shortened by AV, 4-Jan-2022) (Revised by Ender Ting, 29-Jan-2026)

Ref Expression
Hypothesis frgr2wwlkeu.v ⊢ V = Vtx ⁡ G
Assertion frgr2wwlkeu ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → ∃! c ∈ V ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B

Proof

Step Hyp Ref Expression
1 frgr2wwlkeu.v ⊢ V = Vtx ⁡ G
2 df-3an ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B ↔ A ∈ V ∧ B ∈ V ∧ A ≠ B
3 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 1 3 frcond2 ⊢ G ∈ FriendGraph → A ∈ V ∧ B ∈ V ∧ A ≠ B → ∃! c ∈ V A c ∈ Edg ⁡ G ∧ c B ∈ Edg ⁡ G
5 2 4 biimtrrid ⊢ G ∈ FriendGraph → A ∈ V ∧ B ∈ V ∧ A ≠ B → ∃! c ∈ V A c ∈ Edg ⁡ G ∧ c B ∈ Edg ⁡ G
6 5 3impib ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → ∃! c ∈ V A c ∈ Edg ⁡ G ∧ c B ∈ Edg ⁡ G
7 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
8 id ⊢ G ∈ USGraph → G ∈ USGraph
9 3anan32 ⊢ A ∈ V ∧ c ∈ V ∧ B ∈ V ↔ A ∈ V ∧ B ∈ V ∧ c ∈ V
10 1 3 usgrwwlks2on ⊢ G ∈ USGraph ∧ A ∈ V ∧ c ∈ V ∧ B ∈ V → ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B ↔ A c ∈ Edg ⁡ G ∧ c B ∈ Edg ⁡ G
11 10 ex ⊢ G ∈ USGraph → A ∈ V ∧ c ∈ V ∧ B ∈ V → ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B ↔ A c ∈ Edg ⁡ G ∧ c B ∈ Edg ⁡ G
12 9 11 biimtrrid ⊢ G ∈ USGraph → A ∈ V ∧ B ∈ V ∧ c ∈ V → ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B ↔ A c ∈ Edg ⁡ G ∧ c B ∈ Edg ⁡ G
13 7 8 12 3syl ⊢ G ∈ FriendGraph → A ∈ V ∧ B ∈ V ∧ c ∈ V → ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B ↔ A c ∈ Edg ⁡ G ∧ c B ∈ Edg ⁡ G
14 13 impl ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ c ∈ V → ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B ↔ A c ∈ Edg ⁡ G ∧ c B ∈ Edg ⁡ G
15 14 reubidva ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V → ∃! c ∈ V ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B ↔ ∃! c ∈ V A c ∈ Edg ⁡ G ∧ c B ∈ Edg ⁡ G
16 15 3adant3 ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → ∃! c ∈ V ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B ↔ ∃! c ∈ V A c ∈ Edg ⁡ G ∧ c B ∈ Edg ⁡ G
17 6 16 mpbird ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → ∃! c ∈ V ⟨“ AcB ”⟩ ∈ A 2 WWalksNOn G B