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∈Vab∈E∧bc∈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∈Vbabc⊆E
4 reurex ⊢∃!b∈Vbabc⊆E→∃b∈Vbabc⊆E
5 prcom ⊢ab=ba
6 5 eleq1i ⊢ab∈E↔ba∈E
7 6 anbi1i ⊢ab∈E∧bc∈E↔ba∈E∧bc∈E
8 zfpair2 ⊢ba∈V
9 zfpair2 ⊢bc∈V
10 8 9 prss ⊢ba∈E∧bc∈E↔babc⊆E
11 7 10 sylbbr ⊢babc⊆E→ab∈E∧bc∈E
12 11 reximi ⊢∃b∈Vbabc⊆E→∃b∈Vab∈E∧bc∈E
13 4 12 syl ⊢∃!b∈Vbabc⊆E→∃b∈Vab∈E∧bc∈E
14 13 a1i ⊢G∈USGraph∧a∈V∧c∈V∖a→∃!b∈Vbabc⊆E→∃b∈Vab∈E∧bc∈E
15 14 ralimdvva ⊢G∈USGraph→∀a∈V∀c∈V∖a∃!b∈Vbabc⊆E→∀a∈V∀c∈V∖a∃b∈Vab∈E∧bc∈E
16 15 imp ⊢G∈USGraph∧∀a∈V∀c∈V∖a∃!b∈Vbabc⊆E→∀a∈V∀c∈V∖a∃b∈Vab∈E∧bc∈E
17 3 16 sylbi ⊢G∈FriendGraph→∀a∈V∀c∈V∖a∃b∈Vab∈E∧bc∈E