Metamath Proof Explorer

Theorem 2pthfrgrrn

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, 15-Nov-2017) (Revised by AV, 1-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 2pthfrgrrn.v ⊢ V = Vtx ⁡ G
2 2pthfrgrrn.e ⊢ E = Edg ⁡ G
3 1 2 isfrgr ⊢ G ∈ FriendGraph ↔ G ∈ USGraph ∧ ∀ a ∈ V ∀ c ∈ V ∖ a ∃! b ∈ V b a b c ⊆ E
4 reurex ⊢ ∃! b ∈ V b a b c ⊆ E → ∃ b ∈ V b a b c ⊆ E
5 prcom ⊢ a b = b a
6 5 eleq1i ⊢ a b ∈ E ↔ b a ∈ E
7 6 anbi1i ⊢ a b ∈ E ∧ b c ∈ E ↔ b a ∈ E ∧ b c ∈ E
8 zfpair2 ⊢ b a ∈ V
9 zfpair2 ⊢ b c ∈ V
10 8 9 prss ⊢ b a ∈ E ∧ b c ∈ E ↔ b a b c ⊆ E
11 7 10 sylbbr ⊢ b a b c ⊆ E → a b ∈ E ∧ b c ∈ E
12 11 reximi ⊢ ∃ b ∈ V b a b c ⊆ E → ∃ b ∈ V a b ∈ E ∧ b c ∈ E
13 4 12 syl ⊢ ∃! b ∈ V b a b c ⊆ E → ∃ b ∈ V a b ∈ E ∧ b c ∈ E
14 13 a1i ⊢ G ∈ USGraph ∧ a ∈ V ∧ c ∈ V ∖ a → ∃! b ∈ V b a b c ⊆ E → ∃ b ∈ V a b ∈ E ∧ b c ∈ E
15 14 ralimdvva ⊢ G ∈ USGraph → ∀ a ∈ V ∀ c ∈ V ∖ a ∃! b ∈ V b a b c ⊆ E → ∀ a ∈ V ∀ c ∈ V ∖ a ∃ b ∈ V a b ∈ E ∧ b c ∈ E
16 15 imp ⊢ G ∈ USGraph ∧ ∀ a ∈ V ∀ c ∈ V ∖ a ∃! b ∈ V b a b c ⊆ E → ∀ a ∈ V ∀ c ∈ V ∖ a ∃ b ∈ V a b ∈ E ∧ b c ∈ E
17 3 16 sylbi ⊢ G ∈ FriendGraph → ∀ a ∈ V ∀ c ∈ V ∖ a ∃ b ∈ V a b ∈ E ∧ b c ∈ E