Metamath Proof Explorer

Theorem wlkeq

Description: Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018) (Revised by AV, 16-May-2019) (Revised by AV, 14-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 eqid 
 |-  ( 1st ` A ) = ( 1st ` A )
4 eqid 
 |-  ( 2nd ` A ) = ( 2nd ` A )
5 1 2 3 4 wlkelwrd 
 |-  ( A e. ( Walks ` G ) -> ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) ) )
6 eqid 
 |-  ( 1st ` B ) = ( 1st ` B )
7 eqid 
 |-  ( 2nd ` B ) = ( 2nd ` B )
8 1 2 6 7 wlkelwrd 
 |-  ( B e. ( Walks ` G ) -> ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) ) )
9 5 8 anim12i 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) -> ( ( ( 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 ) ) ) )
10 wlkop 
 |-  ( A e. ( Walks ` G ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
11 eleq1 
 |-  ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. -> ( A e. ( Walks ` G ) <-> <. ( 1st ` A ) , ( 2nd ` A ) >. e. ( Walks ` G ) ) )
12 df-br 
 |-  ( ( 1st ` A ) ( Walks ` G ) ( 2nd ` A ) <-> <. ( 1st ` A ) , ( 2nd ` A ) >. e. ( Walks ` G ) )
13 wlklenvm1 
 |-  ( ( 1st ` A ) ( Walks ` G ) ( 2nd ` A ) -> ( # ` ( 1st ` A ) ) = ( ( # ` ( 2nd ` A ) ) - 1 ) )
14 12 13 sylbir 
 |-  ( <. ( 1st ` A ) , ( 2nd ` A ) >. e. ( Walks ` G ) -> ( # ` ( 1st ` A ) ) = ( ( # ` ( 2nd ` A ) ) - 1 ) )
15 11 14 biimtrdi 
 |-  ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. -> ( A e. ( Walks ` G ) -> ( # ` ( 1st ` A ) ) = ( ( # ` ( 2nd ` A ) ) - 1 ) ) )
16 10 15 mpcom 
 |-  ( A e. ( Walks ` G ) -> ( # ` ( 1st ` A ) ) = ( ( # ` ( 2nd ` A ) ) - 1 ) )
17 wlkop 
 |-  ( B e. ( Walks ` G ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
18 eleq1 
 |-  ( B = <. ( 1st ` B ) , ( 2nd ` B ) >. -> ( B e. ( Walks ` G ) <-> <. ( 1st ` B ) , ( 2nd ` B ) >. e. ( Walks ` G ) ) )
19 df-br 
 |-  ( ( 1st ` B ) ( Walks ` G ) ( 2nd ` B ) <-> <. ( 1st ` B ) , ( 2nd ` B ) >. e. ( Walks ` G ) )
20 wlklenvm1 
 |-  ( ( 1st ` B ) ( Walks ` G ) ( 2nd ` B ) -> ( # ` ( 1st ` B ) ) = ( ( # ` ( 2nd ` B ) ) - 1 ) )
21 19 20 sylbir 
 |-  ( <. ( 1st ` B ) , ( 2nd ` B ) >. e. ( Walks ` G ) -> ( # ` ( 1st ` B ) ) = ( ( # ` ( 2nd ` B ) ) - 1 ) )
22 18 21 biimtrdi 
 |-  ( B = <. ( 1st ` B ) , ( 2nd ` B ) >. -> ( B e. ( Walks ` G ) -> ( # ` ( 1st ` B ) ) = ( ( # ` ( 2nd ` B ) ) - 1 ) ) )
23 17 22 mpcom 
 |-  ( B e. ( Walks ` G ) -> ( # ` ( 1st ` B ) ) = ( ( # ` ( 2nd ` B ) ) - 1 ) )
24 16 23 anim12i 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) -> ( ( # ` ( 1st ` A ) ) = ( ( # ` ( 2nd ` A ) ) - 1 ) /\ ( # ` ( 1st ` B ) ) = ( ( # ` ( 2nd ` B ) ) - 1 ) ) )
25 eqwrd 
 |-  ( ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 1st ` B ) e. Word dom ( iEdg ` G ) ) -> ( ( 1st ` A ) = ( 1st ` B ) <-> ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) ) )
26 25 ad2ant2r 
 |-  ( ( ( ( 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 ) ) ) -> ( ( 1st ` A ) = ( 1st ` B ) <-> ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) ) )
27 26 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 ) ) ) /\ ( ( # ` ( 1st ` A ) ) = ( ( # ` ( 2nd ` A ) ) - 1 ) /\ ( # ` ( 1st ` B ) ) = ( ( # ` ( 2nd ` B ) ) - 1 ) ) ) -> ( ( 1st ` A ) = ( 1st ` B ) <-> ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) ) )
28 lencl 
 |-  ( ( 1st ` A ) e. Word dom ( iEdg ` G ) -> ( # ` ( 1st ` A ) ) e. NN0 )
29 28 adantr 
 |-  ( ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) ) -> ( # ` ( 1st ` A ) ) e. NN0 )
30 simpr 
 |-  ( ( ( 1st ` A ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) ) -> ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) )
31 simpr 
 |-  ( ( ( 1st ` B ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) ) -> ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) )
32 2ffzeq 
 |-  ( ( ( # ` ( 1st ` A ) ) e. NN0 /\ ( 2nd ` A ) : ( 0 ... ( # ` ( 1st ` A ) ) ) --> ( Vtx ` G ) /\ ( 2nd ` B ) : ( 0 ... ( # ` ( 1st ` B ) ) ) --> ( Vtx ` G ) ) -> ( ( 2nd ` A ) = ( 2nd ` B ) <-> ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... ( # ` ( 1st ` A ) ) ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) )
33 29 30 31 32 syl2an3an 
 |-  ( ( ( ( 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 ) ) ) -> ( ( 2nd ` A ) = ( 2nd ` B ) <-> ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... ( # ` ( 1st ` A ) ) ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) )
34 33 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 ) ) ) /\ ( ( # ` ( 1st ` A ) ) = ( ( # ` ( 2nd ` A ) ) - 1 ) /\ ( # ` ( 1st ` B ) ) = ( ( # ` ( 2nd ` B ) ) - 1 ) ) ) -> ( ( 2nd ` A ) = ( 2nd ` B ) <-> ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... ( # ` ( 1st ` A ) ) ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) )
35 27 34 anbi12d 
 |-  ( ( ( ( ( 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 ) ) ) /\ ( ( # ` ( 1st ` A ) ) = ( ( # ` ( 2nd ` A ) ) - 1 ) /\ ( # ` ( 1st ` B ) ) = ( ( # ` ( 2nd ` B ) ) - 1 ) ) ) -> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> ( ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... ( # ` ( 1st ` A ) ) ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) ) )
36 9 24 35 syl2anc 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) -> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> ( ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... ( # ` ( 1st ` A ) ) ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) ) )
37 36 3adant3 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> ( ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... ( # ` ( 1st ` A ) ) ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) ) )
38 eqeq1 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( N = ( # ` ( 1st ` B ) ) <-> ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) ) )
39 oveq2 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( 0 ..^ N ) = ( 0 ..^ ( # ` ( 1st ` A ) ) ) )
40 39 raleqdv 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) <-> A. x e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) )
41 38 40 anbi12d 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) <-> ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) ) )
42 oveq2 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( 0 ... N ) = ( 0 ... ( # ` ( 1st ` A ) ) ) )
43 42 raleqdv 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) <-> A. x e. ( 0 ... ( # ` ( 1st ` A ) ) ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) )
44 38 43 anbi12d 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) <-> ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... ( # ` ( 1st ` A ) ) ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) )
45 41 44 anbi12d 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( ( ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) <-> ( ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... ( # ` ( 1st ` A ) ) ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) ) )
46 45 bibi2d 
 |-  ( N = ( # ` ( 1st ` A ) ) -> ( ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> ( ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) ) <-> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> ( ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... ( # ` ( 1st ` A ) ) ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) ) ) )
47 46 3ad2ant3 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> ( ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) ) <-> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> ( ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ ( # ` ( 1st ` A ) ) ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( ( # ` ( 1st ` A ) ) = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... ( # ` ( 1st ` A ) ) ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) ) ) )
48 37 47 mpbird 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> ( ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) ) )
49 1st2ndb 
 |-  ( A e. ( _V X. _V ) <-> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
50 10 49 sylibr 
 |-  ( A e. ( Walks ` G ) -> A e. ( _V X. _V ) )
51 1st2ndb 
 |-  ( B e. ( _V X. _V ) <-> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
52 17 51 sylibr 
 |-  ( B e. ( Walks ` G ) -> B e. ( _V X. _V ) )
53 xpopth 
 |-  ( ( A e. ( _V X. _V ) /\ B e. ( _V X. _V ) ) -> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> A = B ) )
54 50 52 53 syl2an 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) -> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> A = B ) )
55 54 3adant3 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> A = B ) )
56 3anass 
 |-  ( ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) <-> ( N = ( # ` ( 1st ` B ) ) /\ ( A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) )
57 anandi 
 |-  ( ( N = ( # ` ( 1st ` B ) ) /\ ( A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) <-> ( ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) )
58 56 57 bitr2i 
 |-  ( ( ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) <-> ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) )
59 58 a1i 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( ( ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) ) /\ ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) <-> ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) )
60 48 55 59 3bitr3d 
 |-  ( ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = ( # ` ( 1st ` B ) ) /\ A. x e. ( 0 ..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) )