Metamath Proof Explorer

Theorem uspgr2wlkeq

Description: Conditions for two walks within the same simple pseudograph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018) (Revised by AV, 14-Apr-2021)

Ref Expression
Assertion uspgr2wlkeq 
|- ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) ) )

Proof

Step Hyp Ref Expression
1 3anan32 
 |-  ( ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ..^ N ) ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) <-> ( ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) /\ A. y e. ( 0 ..^ N ) ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) ) )
2 1 a1i 
 |-  ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ..^ N ) ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) <-> ( ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) /\ A. y e. ( 0 ..^ N ) ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) ) ) )
3 wlkeq 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ..^ N ) ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) ) )
4 3 3expa 
 |-  ( ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ..^ N ) ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) ) )
5 4 3adant1 
 |-  ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ..^ N ) ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) ) )
6 fzofzp1 
 |-  ( x e. ( 0 ..^ N ) -> ( x + 1 ) e. ( 0 ... N ) )
7 6 adantl 
 |-  ( ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ x e. ( 0 ..^ N ) ) -> ( x + 1 ) e. ( 0 ... N ) )
8 fveq2 
 |-  ( y = ( x + 1 ) -> ( ( 2nd ` A ) ` y ) = ( ( 2nd ` A ) ` ( x + 1 ) ) )
9 fveq2 
 |-  ( y = ( x + 1 ) -> ( ( 2nd ` B ) ` y ) = ( ( 2nd ` B ) ` ( x + 1 ) ) )
10 8 9 eqeq12d 
 |-  ( y = ( x + 1 ) -> ( ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) <-> ( ( 2nd ` A ) ` ( x + 1 ) ) = ( ( 2nd ` B ) ` ( x + 1 ) ) ) )
11 10 adantl 
 |-  ( ( ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ x e. ( 0 ..^ N ) ) /\ y = ( x + 1 ) ) -> ( ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) <-> ( ( 2nd ` A ) ` ( x + 1 ) ) = ( ( 2nd ` B ) ` ( x + 1 ) ) ) )
12 7 11 rspcdv 
 |-  ( ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ x e. ( 0 ..^ N ) ) -> ( A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) -> ( ( 2nd ` A ) ` ( x + 1 ) ) = ( ( 2nd ` B ) ` ( x + 1 ) ) ) )
13 12 impancom 
 |-  ( ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) -> ( x e. ( 0 ..^ N ) -> ( ( 2nd ` A ) ` ( x + 1 ) ) = ( ( 2nd ` B ) ` ( x + 1 ) ) ) )
14 13 ralrimiv 
 |-  ( ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) -> A. x e. ( 0 ..^ N ) ( ( 2nd ` A ) ` ( x + 1 ) ) = ( ( 2nd ` B ) ` ( x + 1 ) ) )
15 fvoveq1 
 |-  ( y = x -> ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` A ) ` ( x + 1 ) ) )
16 fvoveq1 
 |-  ( y = x -> ( ( 2nd ` B ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( x + 1 ) ) )
17 15 16 eqeq12d 
 |-  ( y = x -> ( ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) <-> ( ( 2nd ` A ) ` ( x + 1 ) ) = ( ( 2nd ` B ) ` ( x + 1 ) ) ) )
18 17 cbvralvw 
 |-  ( A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) <-> A. x e. ( 0 ..^ N ) ( ( 2nd ` A ) ` ( x + 1 ) ) = ( ( 2nd ` B ) ` ( x + 1 ) ) )
19 14 18 sylibr 
 |-  ( ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) -> A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) )
20 fzossfz 
 |-  ( 0 ..^ N ) C_ ( 0 ... N )
21 ssralv 
 |-  ( ( 0 ..^ N ) C_ ( 0 ... N ) -> ( A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) -> A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) )
22 20 21 mp1i 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) -> A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) )
23 r19.26 
 |-  ( A. y e. ( 0 ..^ N ) ( ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) /\ ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) ) <-> ( A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) /\ A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) ) )
24 preq12 
 |-  ( ( ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) /\ ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) ) -> { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } )
25 24 a1i 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( ( ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) /\ ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) ) -> { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) )
26 25 ralimdv 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ..^ N ) ( ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) /\ ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) ) -> A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) )
27 23 26 biimtrrid 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( ( A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) /\ A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) ) -> A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) )
28 27 expd 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) -> ( A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) -> A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) ) )
29 22 28 syld 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) -> ( A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) -> A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) ) )
30 29 imp 
 |-  ( ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) -> ( A. y e. ( 0 ..^ N ) ( ( 2nd ` A ) ` ( y + 1 ) ) = ( ( 2nd ` B ) ` ( y + 1 ) ) -> A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) )
31 19 30 mpd 
 |-  ( ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) -> A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } )
32 31 ex 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) -> A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) )
33 uspgrupgr 
 |-  ( G e. USPGraph -> G e. UPGraph )
34 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
35 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
36 eqid 
 |-  ( 1st ` A ) = ( 1st ` A )
37 eqid 
 |-  ( 2nd ` A ) = ( 2nd ` A )
38 34 35 36 37 upgrwlkcompim 
 |-  ( ( G e. UPGraph /\ A e. ( Walks ` G ) ) -> ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) )
39 38 ex 
 |-  ( G e. UPGraph -> ( A e. ( Walks ` G ) -> ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) ) )
40 33 39 syl 
 |-  ( G e. USPGraph -> ( A e. ( Walks ` G ) -> ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) ) )
41 eqid 
 |-  ( 1st ` B ) = ( 1st ` B )
42 eqid 
 |-  ( 2nd ` B ) = ( 2nd ` B )
43 34 35 41 42 upgrwlkcompim 
 |-  ( ( G e. UPGraph /\ B e. ( Walks ` G ) ) -> ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) )
44 43 ex 
 |-  ( G e. UPGraph -> ( B e. ( Walks ` G ) -> ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) ) )
45 33 44 syl 
 |-  ( G e. USPGraph -> ( B e. ( Walks ` G ) -> ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) ) )
46 oveq2 
 |-  ( ( # ` ( 1st ` B ) ) = N -> ( 0 ..^ ( # ` ( 1st ` B ) ) ) = ( 0 ..^ N ) )
47 46 eqcoms 
 |-  ( N = ( # ` ( 1st ` B ) ) -> ( 0 ..^ ( # ` ( 1st ` B ) ) ) = ( 0 ..^ N ) )
48 47 raleqdv 
 |-  ( N = ( # ` ( 1st ` B ) ) -> ( A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } <-> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) )
49 oveq2 
 |-  ( ( # ` ( 1st ` A ) ) = N -> ( 0 ..^ ( # ` ( 1st ` A ) ) ) = ( 0 ..^ N ) )
50 49 eqcoms 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( 0 ..^ ( # ` ( 1st ` A ) ) ) = ( 0 ..^ N ) )
51 50 raleqdv 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } <-> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) )
52 48 51 bi2anan9r 
 |-  ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( ( A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } /\ A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) <-> ( A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } /\ A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) ) )
53 r19.26 
 |-  ( A. y e. ( 0 ..^ N ) ( ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } /\ ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) <-> ( A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } /\ A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) )
54 eqeq2 
 |-  ( { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> ( ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } <-> ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) )
55 eqeq2 
 |-  ( { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) -> ( ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } <-> ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) )
56 55 eqcoms 
 |-  ( ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> ( ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } <-> ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) )
57 56 biimpd 
 |-  ( ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> ( ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) )
58 54 57 biimtrdi 
 |-  ( { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> ( ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } -> ( ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) )
59 58 com13 
 |-  ( ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> ( ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } -> ( { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) )
60 59 imp 
 |-  ( ( ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } /\ ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) -> ( { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) )
61 60 ral2imi 
 |-  ( A. y e. ( 0 ..^ N ) ( ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } /\ ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) )
62 53 61 sylbir 
 |-  ( ( A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } /\ A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) )
63 52 62 biimtrdi 
 |-  ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( ( A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } /\ A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) )
64 63 com12 
 |-  ( ( A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } /\ A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) -> ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) )
65 64 ex 
 |-  ( A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> ( A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } -> ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) ) )
66 65 3ad2ant3 
 |-  ( ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) -> ( A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } -> ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) ) )
67 66 com12 
 |-  ( A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } -> ( ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) -> ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) ) )
68 67 3ad2ant3 
 |-  ( ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) -> ( ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) -> ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) ) )
69 68 imp 
 |-  ( ( ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) /\ ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) ) -> ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) )
70 69 expd 
 |-  ( ( ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) /\ ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) ) -> ( N = ( # ` ( 1st ` A ) ) -> ( N = ( # ` ( 1st ` B ) ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) ) )
71 70 a1i 
 |-  ( G e. USPGraph -> ( ( ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } ) /\ ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) /\ A. y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } ) ) -> ( N = ( # ` ( 1st ` A ) ) -> ( N = ( # ` ( 1st ` B ) ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) ) ) )
72 40 45 71 syl2and 
 |-  ( G e. USPGraph -> ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) -> ( N = ( # ` ( 1st ` A ) ) -> ( N = ( # ` ( 1st ` B ) ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) ) ) ) )
73 72 3imp1 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ..^ N ) { ( ( 2nd ` A ) ` y ) , ( ( 2nd ` A ) ` ( y + 1 ) ) } = { ( ( 2nd ` B ) ` y ) , ( ( 2nd ` B ) ` ( y + 1 ) ) } -> A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) ) )
74 eqcom 
 |-  ( ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) <-> ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) )
75 35 uspgrf1oedg 
 |-  ( G e. USPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) )
76 f1of1 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) )
77 75 76 syl 
 |-  ( G e. USPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) )
78 eqidd 
 |-  ( G e. USPGraph -> ( iEdg ` G ) = ( iEdg ` G ) )
79 eqidd 
 |-  ( G e. USPGraph -> dom ( iEdg ` G ) = dom ( iEdg ` G ) )
80 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
81 80 eqcomi 
 |-  ran ( iEdg ` G ) = ( Edg ` G )
82 81 a1i 
 |-  ( G e. USPGraph -> ran ( iEdg ` G ) = ( Edg ` G ) )
83 78 79 82 f1eq123d 
 |-  ( G e. USPGraph -> ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ran ( iEdg ` G ) <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) ) )
84 77 83 mpbird 
 |-  ( G e. USPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ran ( iEdg ` G ) )
85 84 3ad2ant1 
 |-  ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ran ( iEdg ` G ) )
86 85 adantr 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ran ( iEdg ` G ) )
87 34 35 36 37 wlkelwrd 
 |-  ( A e. ( Walks ` G ) -> ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) ) )
88 34 35 41 42 wlkelwrd 
 |-  ( B e. ( Walks ` G ) -> ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) ) )
89 oveq2 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( 0 ..^ N ) = ( 0 ..^ ( # ` ( 1st ` A ) ) ) )
90 89 eleq2d 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( y e. ( 0 ..^ N ) <-> y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ) )
91 wrdsymbcl 
 |-  ( ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ) -> ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) )
92 91 expcom 
 |-  ( y e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) -> ( ( 1st ` A ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) ) )
93 90 92 biimtrdi 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( y e. ( 0 ..^ N ) -> ( ( 1st ` A ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) ) ) )
94 93 adantr 
 |-  ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( y e. ( 0 ..^ N ) -> ( ( 1st ` A ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) ) ) )
95 94 imp 
 |-  ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( 1st ` A ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) ) )
96 95 com12 
 |-  ( ( 1st ` A ) e. Word dom ( iEdg ` G ) -> ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) ) )
97 96 adantl 
 |-  ( ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 1st ` A ) e. Word dom ( iEdg ` G ) ) -> ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) ) )
98 oveq2 
 |-  ( N = ( # ` ( 1st ` B ) ) -> ( 0 ..^ N ) = ( 0 ..^ ( # ` ( 1st ` B ) ) ) )
99 98 eleq2d 
 |-  ( N = ( # ` ( 1st ` B ) ) -> ( y e. ( 0 ..^ N ) <-> y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ) )
100 wrdsymbcl 
 |-  ( ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) ) -> ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) )
101 100 expcom 
 |-  ( y e. ( 0 ..^ ( # ` ( 1st ` B ) ) ) -> ( ( 1st ` B ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) )
102 99 101 biimtrdi 
 |-  ( N = ( # ` ( 1st ` B ) ) -> ( y e. ( 0 ..^ N ) -> ( ( 1st ` B ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) )
103 102 adantl 
 |-  ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( y e. ( 0 ..^ N ) -> ( ( 1st ` B ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) )
104 103 imp 
 |-  ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( 1st ` B ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) )
105 104 com12 
 |-  ( ( 1st ` B ) e. Word dom ( iEdg ` G ) -> ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) )
106 105 adantr 
 |-  ( ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 1st ` A ) e. Word dom ( iEdg ` G ) ) -> ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) )
107 97 106 jcad 
 |-  ( ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 1st ` A ) e. Word dom ( iEdg ` G ) ) -> ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) )
108 107 ex 
 |-  ( ( 1st ` B ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` A ) e. Word dom ( iEdg ` G ) -> ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) ) )
109 108 adantr 
 |-  ( ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) ) -> ( ( 1st ` A ) e. Word dom ( iEdg ` G ) -> ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) ) )
110 109 com12 
 |-  ( ( 1st ` A ) e. Word dom ( iEdg ` G ) -> ( ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) ) -> ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) ) )
111 110 adantr 
 |-  ( ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) ) -> ( ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) ) -> ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) ) )
112 111 imp 
 |-  ( ( ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) ) /\ ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) ) ) -> ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) )
113 87 88 112 syl2an 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) -> ( ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) )
114 113 expd 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) -> ( ( N = ( # ` ( 1st ` A ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( y e. ( 0 ..^ N ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) ) )
115 114 expd 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) -> ( N = ( # ` ( 1st ` A ) ) -> ( N = ( # ` ( 1st ` B ) ) -> ( y e. ( 0 ..^ N ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) ) ) )
116 115 imp 
 |-  ( ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( N = ( # ` ( 1st ` B ) ) -> ( y e. ( 0 ..^ N ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) ) )
117 116 3adant1 
 |-  ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( N = ( # ` ( 1st ` B ) ) -> ( y e. ( 0 ..^ N ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) ) )
118 117 imp 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( y e. ( 0 ..^ N ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) )
119 118 imp 
 |-  ( ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) )
120 f1veqaeq 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ran ( iEdg ` G ) /\ ( ( ( 1st ` A ) ` y ) e. dom ( iEdg ` G ) /\ ( ( 1st ` B ) ` y ) e. dom ( iEdg ` G ) ) ) -> ( ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) -> ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) ) )
121 86 119 120 syl2an2r 
 |-  ( ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) -> ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) ) )
122 74 121 biimtrid 
 |-  ( ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) -> ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) ) )
123 122 ralimdva 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ..^ N ) ( ( iEdg ` G ) ` ( ( 1st ` B ) ` y ) ) = ( ( iEdg ` G ) ` ( ( 1st ` A ) ` y ) ) -> A. y e. ( 0 ..^ N ) ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) ) )
124 32 73 123 3syld 
 |-  ( ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) /\ N = ( # ` ( 1st ` B ) ) ) -> ( A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) -> A. y e. ( 0 ..^ N ) ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) ) )
125 124 expimpd 
 |-  ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) -> A. y e. ( 0 ..^ N ) ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) ) )
126 125 pm4.71d 
 |-  ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) <-> ( ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) /\ A. y e. ( 0 ..^ N ) ( ( 1st ` A ) ` y ) = ( ( 1st ` B ) ` y ) ) ) )
127 2 5 126 3bitr4d 
 |-  ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) ) )