Metamath Proof Explorer

Theorem 2pthfrgrrn2

Description: Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1(b) of MertziosUnger p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 16-Nov-2017) (Revised by AV, 1-Apr-2021)

Ref Expression
Hypotheses 2pthfrgrrn.v ⊢ V = Vtx ⁡ G
2pthfrgrrn.e ⊢ E = Edg ⁡ G
Assertion 2pthfrgrrn2 ⊢ G ∈ FriendGraph → ∀ a ∈ V ∀ c ∈ V ∖ a ∃ b ∈ V a b ∈ E ∧ b c ∈ E ∧ a ≠ b ∧ b ≠ c

Proof

Step Hyp Ref Expression
1 2pthfrgrrn.v ⊢ V = Vtx ⁡ G
2 2pthfrgrrn.e ⊢ E = Edg ⁡ G
3 1 2 2pthfrgrrn ⊢ G ∈ FriendGraph → ∀ a ∈ V ∀ c ∈ V ∖ a ∃ b ∈ V a b ∈ E ∧ b c ∈ E
4 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
5 2 usgredgne ⊢ G ∈ USGraph ∧ a b ∈ E → a ≠ b
6 5 ex ⊢ G ∈ USGraph → a b ∈ E → a ≠ b
7 2 usgredgne ⊢ G ∈ USGraph ∧ b c ∈ E → b ≠ c
8 7 ex ⊢ G ∈ USGraph → b c ∈ E → b ≠ c
9 6 8 anim12d ⊢ G ∈ USGraph → a b ∈ E ∧ b c ∈ E → a ≠ b ∧ b ≠ c
10 4 9 syl ⊢ G ∈ FriendGraph → a b ∈ E ∧ b c ∈ E → a ≠ b ∧ b ≠ c
11 10 ad2antrr ⊢ G ∈ FriendGraph ∧ a ∈ V ∧ c ∈ V ∖ a ∧ b ∈ V → a b ∈ E ∧ b c ∈ E → a ≠ b ∧ b ≠ c
12 11 ancld ⊢ G ∈ FriendGraph ∧ a ∈ V ∧ c ∈ V ∖ a ∧ b ∈ V → a b ∈ E ∧ b c ∈ E → a b ∈ E ∧ b c ∈ E ∧ a ≠ b ∧ b ≠ c
13 12 reximdva ⊢ G ∈ FriendGraph ∧ a ∈ V ∧ c ∈ V ∖ a → ∃ b ∈ V a b ∈ E ∧ b c ∈ E → ∃ b ∈ V a b ∈ E ∧ b c ∈ E ∧ a ≠ b ∧ b ≠ c
14 13 ralimdvva ⊢ G ∈ FriendGraph → ∀ a ∈ V ∀ c ∈ V ∖ a ∃ b ∈ V a b ∈ E ∧ b c ∈ E → ∀ a ∈ V ∀ c ∈ V ∖ a ∃ b ∈ V a b ∈ E ∧ b c ∈ E ∧ a ≠ b ∧ b ≠ c
15 3 14 mpd ⊢ G ∈ FriendGraph → ∀ a ∈ V ∀ c ∈ V ∖ a ∃ b ∈ V a b ∈ E ∧ b c ∈ E ∧ a ≠ b ∧ b ≠ c