Metamath Proof Explorer

Theorem frgr2wwlk1

Description: In a friendship graph, there is exactly one walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018) (Revised by AV, 13-May-2021) (Proof shortened by AV, 16-Mar-2022)

Ref Expression
Hypothesis frgr2wwlkeu.v 
|- V = ( Vtx ` G )
Assertion frgr2wwlk1 
|- ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( # ` ( A ( 2 WWalksNOn G ) B ) ) = 1 )

Proof

Step Hyp Ref Expression
1 frgr2wwlkeu.v 
 |-  V = ( Vtx ` G )
2 1 frgr2wwlkn0 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( A ( 2 WWalksNOn G ) B ) =/= (/) )
3 1 elwwlks2ons3 
 |-  ( w e. ( A ( 2 WWalksNOn G ) B ) <-> E. d e. V ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) )
4 1 elwwlks2ons3 
 |-  ( t e. ( A ( 2 WWalksNOn G ) B ) <-> E. c e. V ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) )
5 3 4 anbi12i 
 |-  ( ( w e. ( A ( 2 WWalksNOn G ) B ) /\ t e. ( A ( 2 WWalksNOn G ) B ) ) <-> ( E. d e. V ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) /\ E. c e. V ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) ) )
6 1 frgr2wwlkeu 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> E! x e. V <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) )
7 s3eq2 
 |-  ( x = y -> <" A x B "> = <" A y B "> )
8 7 eleq1d 
 |-  ( x = y -> ( <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) <-> <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) ) )
9 8 reu4 
 |-  ( E! x e. V <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) <-> ( E. x e. V <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) /\ A. x e. V A. y e. V ( ( <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> x = y ) ) )
10 s3eq2 
 |-  ( x = d -> <" A x B "> = <" A d B "> )
11 10 eleq1d 
 |-  ( x = d -> ( <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) <-> <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) )
12 11 anbi1d 
 |-  ( x = d -> ( ( <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) ) <-> ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) ) ) )
13 equequ1 
 |-  ( x = d -> ( x = y <-> d = y ) )
14 12 13 imbi12d 
 |-  ( x = d -> ( ( ( <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> x = y ) <-> ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = y ) ) )
15 s3eq2 
 |-  ( y = c -> <" A y B "> = <" A c B "> )
16 15 eleq1d 
 |-  ( y = c -> ( <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) <-> <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) )
17 16 anbi2d 
 |-  ( y = c -> ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) ) <-> ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) ) )
18 equequ2 
 |-  ( y = c -> ( d = y <-> d = c ) )
19 17 18 imbi12d 
 |-  ( y = c -> ( ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = y ) <-> ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) ) )
20 14 19 rspc2va 
 |-  ( ( ( d e. V /\ c e. V ) /\ A. x e. V A. y e. V ( ( <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> x = y ) ) -> ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) )
21 pm3.35 
 |-  ( ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) /\ ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) ) -> d = c )
22 s3eq2 
 |-  ( c = d -> <" A c B "> = <" A d B "> )
23 22 equcoms 
 |-  ( d = c -> <" A c B "> = <" A d B "> )
24 23 adantr 
 |-  ( ( d = c /\ ( t = <" A c B "> /\ w = <" A d B "> ) ) -> <" A c B "> = <" A d B "> )
25 eqeq12 
 |-  ( ( t = <" A c B "> /\ w = <" A d B "> ) -> ( t = w <-> <" A c B "> = <" A d B "> ) )
26 25 adantl 
 |-  ( ( d = c /\ ( t = <" A c B "> /\ w = <" A d B "> ) ) -> ( t = w <-> <" A c B "> = <" A d B "> ) )
27 24 26 mpbird 
 |-  ( ( d = c /\ ( t = <" A c B "> /\ w = <" A d B "> ) ) -> t = w )
28 27 equcomd 
 |-  ( ( d = c /\ ( t = <" A c B "> /\ w = <" A d B "> ) ) -> w = t )
29 28 ex 
 |-  ( d = c -> ( ( t = <" A c B "> /\ w = <" A d B "> ) -> w = t ) )
30 21 29 syl 
 |-  ( ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) /\ ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) ) -> ( ( t = <" A c B "> /\ w = <" A d B "> ) -> w = t ) )
31 30 ex 
 |-  ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) -> ( ( t = <" A c B "> /\ w = <" A d B "> ) -> w = t ) ) )
32 31 com23 
 |-  ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( ( t = <" A c B "> /\ w = <" A d B "> ) -> ( ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) -> w = t ) ) )
33 32 exp4b 
 |-  ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) -> ( <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) -> ( t = <" A c B "> -> ( w = <" A d B "> -> ( ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) -> w = t ) ) ) ) )
34 33 com13 
 |-  ( t = <" A c B "> -> ( <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) -> ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) -> ( w = <" A d B "> -> ( ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) -> w = t ) ) ) ) )
35 34 imp 
 |-  ( ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) -> ( w = <" A d B "> -> ( ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) -> w = t ) ) ) )
36 35 com13 
 |-  ( w = <" A d B "> -> ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) -> ( ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) -> w = t ) ) ) )
37 36 imp 
 |-  ( ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) -> w = t ) ) )
38 37 com13 
 |-  ( ( ( <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> d = c ) -> ( ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> w = t ) ) )
39 20 38 syl 
 |-  ( ( ( d e. V /\ c e. V ) /\ A. x e. V A. y e. V ( ( <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> x = y ) ) -> ( ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> w = t ) ) )
40 39 expcom 
 |-  ( A. x e. V A. y e. V ( ( <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" A y B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> x = y ) -> ( ( d e. V /\ c e. V ) -> ( ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> w = t ) ) ) )
41 9 40 simplbiim 
 |-  ( E! x e. V <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) -> ( ( d e. V /\ c e. V ) -> ( ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> w = t ) ) ) )
42 41 impl 
 |-  ( ( ( E! x e. V <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) /\ d e. V ) /\ c e. V ) -> ( ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> w = t ) ) )
43 42 rexlimdva 
 |-  ( ( E! x e. V <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) /\ d e. V ) -> ( E. c e. V ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> w = t ) ) )
44 43 com23 
 |-  ( ( E! x e. V <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) /\ d e. V ) -> ( ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( E. c e. V ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> w = t ) ) )
45 44 rexlimdva 
 |-  ( E! x e. V <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) -> ( E. d e. V ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> ( E. c e. V ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) -> w = t ) ) )
46 45 impd 
 |-  ( E! x e. V <" A x B "> e. ( A ( 2 WWalksNOn G ) B ) -> ( ( E. d e. V ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) /\ E. c e. V ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) ) -> w = t ) )
47 6 46 syl 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( ( E. d e. V ( w = <" A d B "> /\ <" A d B "> e. ( A ( 2 WWalksNOn G ) B ) ) /\ E. c e. V ( t = <" A c B "> /\ <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) ) ) -> w = t ) )
48 5 47 biimtrid 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( ( w e. ( A ( 2 WWalksNOn G ) B ) /\ t e. ( A ( 2 WWalksNOn G ) B ) ) -> w = t ) )
49 48 alrimivv 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> A. w A. t ( ( w e. ( A ( 2 WWalksNOn G ) B ) /\ t e. ( A ( 2 WWalksNOn G ) B ) ) -> w = t ) )
50 eqeuel 
 |-  ( ( ( A ( 2 WWalksNOn G ) B ) =/= (/) /\ A. w A. t ( ( w e. ( A ( 2 WWalksNOn G ) B ) /\ t e. ( A ( 2 WWalksNOn G ) B ) ) -> w = t ) ) -> E! w w e. ( A ( 2 WWalksNOn G ) B ) )
51 2 49 50 syl2anc 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> E! w w e. ( A ( 2 WWalksNOn G ) B ) )
52 ovex 
 |-  ( A ( 2 WWalksNOn G ) B ) e. _V
53 euhash1 
 |-  ( ( A ( 2 WWalksNOn G ) B ) e. _V -> ( ( # ` ( A ( 2 WWalksNOn G ) B ) ) = 1 <-> E! w w e. ( A ( 2 WWalksNOn G ) B ) ) )
54 52 53 mp1i 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( ( # ` ( A ( 2 WWalksNOn G ) B ) ) = 1 <-> E! w w e. ( A ( 2 WWalksNOn G ) B ) ) )
55 51 54 mpbird 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( # ` ( A ( 2 WWalksNOn G ) B ) ) = 1 )