Metamath Proof Explorer

Theorem 2pthfrgr

Description: Between any two (different) vertices in a friendship graph, tere is a 2-path (simple 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, 6-Dec-2017) (Revised by AV, 1-Apr-2021)

Ref Expression
Hypothesis 2pthfrgr.v 
|- V = ( Vtx ` G )
Assertion 2pthfrgr 
|- ( G e. FriendGraph -> A. a e. V A. b e. ( V \ { a } ) E. f E. p ( f ( a ( SPathsOn ` G ) b ) p /\ ( # ` f ) = 2 ) )

Proof

Step Hyp Ref Expression
1 2pthfrgr.v 
 |-  V = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 2pthfrgrrn2 
 |-  ( G e. FriendGraph -> A. a e. V A. b e. ( V \ { a } ) E. m e. V ( ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) /\ ( a =/= m /\ m =/= b ) ) )
4 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
5 usgruhgr 
 |-  ( G e. USGraph -> G e. UHGraph )
6 4 5 syl 
 |-  ( G e. FriendGraph -> G e. UHGraph )
7 6 adantr 
 |-  ( ( G e. FriendGraph /\ a e. V ) -> G e. UHGraph )
8 7 adantr 
 |-  ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) -> G e. UHGraph )
9 8 adantr 
 |-  ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) -> G e. UHGraph )
10 simpllr 
 |-  ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) -> a e. V )
11 simpr 
 |-  ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) -> m e. V )
12 eldifi 
 |-  ( b e. ( V \ { a } ) -> b e. V )
13 12 ad2antlr 
 |-  ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) -> b e. V )
14 10 11 13 3jca 
 |-  ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) -> ( a e. V /\ m e. V /\ b e. V ) )
15 9 14 jca 
 |-  ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) -> ( G e. UHGraph /\ ( a e. V /\ m e. V /\ b e. V ) ) )
16 15 adantr 
 |-  ( ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) /\ ( ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) /\ ( a =/= m /\ m =/= b ) ) ) -> ( G e. UHGraph /\ ( a e. V /\ m e. V /\ b e. V ) ) )
17 simprrl 
 |-  ( ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) /\ ( ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) /\ ( a =/= m /\ m =/= b ) ) ) -> a =/= m )
18 eldifsn 
 |-  ( b e. ( V \ { a } ) <-> ( b e. V /\ b =/= a ) )
19 necom 
 |-  ( b =/= a <-> a =/= b )
20 19 biimpi 
 |-  ( b =/= a -> a =/= b )
21 18 20 simplbiim 
 |-  ( b e. ( V \ { a } ) -> a =/= b )
22 21 ad3antlr 
 |-  ( ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) /\ ( ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) /\ ( a =/= m /\ m =/= b ) ) ) -> a =/= b )
23 simprrr 
 |-  ( ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) /\ ( ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) /\ ( a =/= m /\ m =/= b ) ) ) -> m =/= b )
24 simprl 
 |-  ( ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) /\ ( ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) /\ ( a =/= m /\ m =/= b ) ) ) -> ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) )
25 1 2 2pthon3v 
 |-  ( ( ( G e. UHGraph /\ ( a e. V /\ m e. V /\ b e. V ) ) /\ ( a =/= m /\ a =/= b /\ m =/= b ) /\ ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) ) -> E. f E. p ( f ( a ( SPathsOn ` G ) b ) p /\ ( # ` f ) = 2 ) )
26 16 17 22 23 24 25 syl131anc 
 |-  ( ( ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) /\ m e. V ) /\ ( ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) /\ ( a =/= m /\ m =/= b ) ) ) -> E. f E. p ( f ( a ( SPathsOn ` G ) b ) p /\ ( # ` f ) = 2 ) )
27 26 rexlimdva2 
 |-  ( ( ( G e. FriendGraph /\ a e. V ) /\ b e. ( V \ { a } ) ) -> ( E. m e. V ( ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) /\ ( a =/= m /\ m =/= b ) ) -> E. f E. p ( f ( a ( SPathsOn ` G ) b ) p /\ ( # ` f ) = 2 ) ) )
28 27 ralimdva 
 |-  ( ( G e. FriendGraph /\ a e. V ) -> ( A. b e. ( V \ { a } ) E. m e. V ( ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) /\ ( a =/= m /\ m =/= b ) ) -> A. b e. ( V \ { a } ) E. f E. p ( f ( a ( SPathsOn ` G ) b ) p /\ ( # ` f ) = 2 ) ) )
29 28 ralimdva 
 |-  ( G e. FriendGraph -> ( A. a e. V A. b e. ( V \ { a } ) E. m e. V ( ( { a , m } e. ( Edg ` G ) /\ { m , b } e. ( Edg ` G ) ) /\ ( a =/= m /\ m =/= b ) ) -> A. a e. V A. b e. ( V \ { a } ) E. f E. p ( f ( a ( SPathsOn ` G ) b ) p /\ ( # ` f ) = 2 ) ) )
30 3 29 mpd 
 |-  ( G e. FriendGraph -> A. a e. V A. b e. ( V \ { a } ) E. f E. p ( f ( a ( SPathsOn ` G ) b ) p /\ ( # ` f ) = 2 ) )