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∈Vab∈E∧bc∈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∈Vab∈E∧bc∈E
4 frgrusgr ⊢G∈FriendGraph→G∈USGraph
5 2 usgredgne ⊢G∈USGraph∧ab∈E→a≠b
6 5 ex ⊢G∈USGraph→ab∈E→a≠b
7 2 usgredgne ⊢G∈USGraph∧bc∈E→b≠c
8 7 ex ⊢G∈USGraph→bc∈E→b≠c
9 6 8 anim12d ⊢G∈USGraph→ab∈E∧bc∈E→a≠b∧b≠c
10 4 9 syl ⊢G∈FriendGraph→ab∈E∧bc∈E→a≠b∧b≠c
11 10 ad2antrr ⊢G∈FriendGraph∧a∈V∧c∈V∖a∧b∈V→ab∈E∧bc∈E→a≠b∧b≠c
12 11 ancld ⊢G∈FriendGraph∧a∈V∧c∈V∖a∧b∈V→ab∈E∧bc∈E→ab∈E∧bc∈E∧a≠b∧b≠c
13 12 reximdva ⊢G∈FriendGraph∧a∈V∧c∈V∖a→∃b∈Vab∈E∧bc∈E→∃b∈Vab∈E∧bc∈E∧a≠b∧b≠c
14 13 ralimdvva ⊢G∈FriendGraph→∀a∈V∀c∈V∖a∃b∈Vab∈E∧bc∈E→∀a∈V∀c∈V∖a∃b∈Vab∈E∧bc∈E∧a≠b∧b≠c
15 3 14 mpd ⊢G∈FriendGraph→∀a∈V∀c∈V∖a∃b∈Vab∈E∧bc∈E∧a≠b∧b≠c