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 e. FriendGraph -> A. a e. V A. c e. ( V \ { a } ) E. b e. V ( { a , b } e. E /\ { b , c } e. E ) )

Proof

Step	Hyp	Ref	Expression
1		2pthfrgrrn.v	|- V = ( Vtx ` G )
2		2pthfrgrrn.e	|- E = ( Edg ` G )
3	1 2	isfrgr	|- ( G e. FriendGraph <-> ( G e. USGraph /\ A. a e. V A. c e. ( V \ { a } ) E! b e. V { { b , a } , { b , c } } C_ E ) )
4		reurex	|- ( E! b e. V { { b , a } , { b , c } } C_ E -> E. b e. V { { b , a } , { b , c } } C_ E )
5		prcom	|- { a , b } = { b , a }
6	5	eleq1i	|- ( { a , b } e. E <-> { b , a } e. E )
7	6	anbi1i	|- ( ( { a , b } e. E /\ { b , c } e. E ) <-> ( { b , a } e. E /\ { b , c } e. E ) )
8		zfpair2	|- { b , a } e. _V
9		zfpair2	|- { b , c } e. _V
10	8 9	prss	|- ( ( { b , a } e. E /\ { b , c } e. E ) <-> { { b , a } , { b , c } } C_ E )
11	7 10	sylbbr	|- ( { { b , a } , { b , c } } C_ E -> ( { a , b } e. E /\ { b , c } e. E ) )
12	11	reximi	|- ( E. b e. V { { b , a } , { b , c } } C_ E -> E. b e. V ( { a , b } e. E /\ { b , c } e. E ) )
13	4 12	syl	|- ( E! b e. V { { b , a } , { b , c } } C_ E -> E. b e. V ( { a , b } e. E /\ { b , c } e. E ) )
14	13	a1i	|- ( ( G e. USGraph /\ ( a e. V /\ c e. ( V \ { a } ) ) ) -> ( E! b e. V { { b , a } , { b , c } } C_ E -> E. b e. V ( { a , b } e. E /\ { b , c } e. E ) ) )
15	14	ralimdvva	|- ( G e. USGraph -> ( A. a e. V A. c e. ( V \ { a } ) E! b e. V { { b , a } , { b , c } } C_ E -> A. a e. V A. c e. ( V \ { a } ) E. b e. V ( { a , b } e. E /\ { b , c } e. E ) ) )
16	15	imp	|- ( ( G e. USGraph /\ A. a e. V A. c e. ( V \ { a } ) E! b e. V { { b , a } , { b , c } } C_ E ) -> A. a e. V A. c e. ( V \ { a } ) E. b e. V ( { a , b } e. E /\ { b , c } e. E ) )
17	3 16	sylbi	|- ( G e. FriendGraph -> A. a e. V A. c e. ( V \ { a } ) E. b e. V ( { a , b } e. E /\ { b , c } e. E ) )