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 e. FriendGraph -> A. a e. V A. c e. ( V \ { a } ) E. b e. V ( ( { a , b } e. E /\ { b , c } e. 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 e. FriendGraph -> A. a e. V A. c e. ( V \ { a } ) E. b e. V ( { a , b } e. E /\ { b , c } e. E ) )
4		frgrusgr	|- ( G e. FriendGraph -> G e. USGraph )
5	2	usgredgne	|- ( ( G e. USGraph /\ { a , b } e. E ) -> a =/= b )
6	5	ex	|- ( G e. USGraph -> ( { a , b } e. E -> a =/= b ) )
7	2	usgredgne	|- ( ( G e. USGraph /\ { b , c } e. E ) -> b =/= c )
8	7	ex	|- ( G e. USGraph -> ( { b , c } e. E -> b =/= c ) )
9	6 8	anim12d	|- ( G e. USGraph -> ( ( { a , b } e. E /\ { b , c } e. E ) -> ( a =/= b /\ b =/= c ) ) )
10	4 9	syl	|- ( G e. FriendGraph -> ( ( { a , b } e. E /\ { b , c } e. E ) -> ( a =/= b /\ b =/= c ) ) )
11	10	ad2antrr	|- ( ( ( G e. FriendGraph /\ ( a e. V /\ c e. ( V \ { a } ) ) ) /\ b e. V ) -> ( ( { a , b } e. E /\ { b , c } e. E ) -> ( a =/= b /\ b =/= c ) ) )
12	11	ancld	|- ( ( ( G e. FriendGraph /\ ( a e. V /\ c e. ( V \ { a } ) ) ) /\ b e. V ) -> ( ( { a , b } e. E /\ { b , c } e. E ) -> ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( a =/= b /\ b =/= c ) ) ) )
13	12	reximdva	|- ( ( G e. FriendGraph /\ ( a e. V /\ c e. ( V \ { a } ) ) ) -> ( E. b e. V ( { a , b } e. E /\ { b , c } e. E ) -> E. b e. V ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( a =/= b /\ b =/= c ) ) ) )
14	13	ralimdvva	|- ( G e. FriendGraph -> ( A. a e. V A. c e. ( V \ { a } ) E. b e. V ( { a , b } e. E /\ { b , c } e. E ) -> A. a e. V A. c e. ( V \ { a } ) E. b e. V ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( a =/= b /\ b =/= c ) ) ) )
15	3 14	mpd	|- ( G e. FriendGraph -> A. a e. V A. c e. ( V \ { a } ) E. b e. V ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( a =/= b /\ b =/= c ) ) )