Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) -> ( # ` ( 1st ` B ) ) = N ) |
2 |
1
|
eqcomd |
|- ( ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) -> N = ( # ` ( 1st ` B ) ) ) |
3 |
2
|
3ad2ant3 |
|- ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) -> N = ( # ` ( 1st ` B ) ) ) |
4 |
3
|
adantr |
|- ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> N = ( # ` ( 1st ` B ) ) ) |
5 |
|
fveq1 |
|- ( ( 2nd ` A ) = ( 2nd ` B ) -> ( ( 2nd ` A ) ` i ) = ( ( 2nd ` B ) ` i ) ) |
6 |
5
|
adantl |
|- ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> ( ( 2nd ` A ) ` i ) = ( ( 2nd ` B ) ` i ) ) |
7 |
6
|
ralrimivw |
|- ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> A. i e. ( 0 ... N ) ( ( 2nd ` A ) ` i ) = ( ( 2nd ` B ) ` i ) ) |
8 |
|
simpl1l |
|- ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> G e. USPGraph ) |
9 |
|
simpl |
|- ( ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) -> A e. ( Walks ` G ) ) |
10 |
|
simpl |
|- ( ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) -> B e. ( Walks ` G ) ) |
11 |
9 10
|
anim12i |
|- ( ( ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) -> ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) ) |
12 |
11
|
3adant1 |
|- ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) -> ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) ) |
13 |
12
|
adantr |
|- ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) ) |
14 |
|
simpr |
|- ( ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) -> ( # ` ( 1st ` A ) ) = N ) |
15 |
14
|
eqcomd |
|- ( ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) -> N = ( # ` ( 1st ` A ) ) ) |
16 |
15
|
3ad2ant2 |
|- ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) -> N = ( # ` ( 1st ` A ) ) ) |
17 |
16
|
adantr |
|- ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> N = ( # ` ( 1st ` A ) ) ) |
18 |
|
uspgr2wlkeq |
|- ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = ( # ` ( 1st ` B ) ) /\ A. i e. ( 0 ... N ) ( ( 2nd ` A ) ` i ) = ( ( 2nd ` B ) ` i ) ) ) ) |
19 |
8 13 17 18
|
syl3anc |
|- ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> ( A = B <-> ( N = ( # ` ( 1st ` B ) ) /\ A. i e. ( 0 ... N ) ( ( 2nd ` A ) ` i ) = ( ( 2nd ` B ) ` i ) ) ) ) |
20 |
4 7 19
|
mpbir2and |
|- ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> A = B ) |
21 |
20
|
ex |
|- ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) -> ( ( 2nd ` A ) = ( 2nd ` B ) -> A = B ) ) |