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 syl5bir
 |-  ( ( ( 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 syl6bi
 |-  ( { ( ( 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 syl6bi
 |-  ( ( 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 syl6bi
 |-  ( 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 syl6bi
 |-  ( 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 syl5bi
 |-  ( ( ( ( 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 ) ) ) )