Step |
Hyp |
Ref |
Expression |
1 |
|
clwlkclwwlkf.c |
|- C = { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |
2 |
|
clwlkclwwlkf.f |
|- F = ( c e. C |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) |
3 |
|
eqid |
|- ( 1st ` c ) = ( 1st ` c ) |
4 |
|
eqid |
|- ( 2nd ` c ) = ( 2nd ` c ) |
5 |
1 3 4
|
clwlkclwwlkflem |
|- ( c e. C -> ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) e. NN ) ) |
6 |
|
isclwlk |
|- ( ( 1st ` c ) ( ClWalks ` G ) ( 2nd ` c ) <-> ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) ) ) |
7 |
|
fvex |
|- ( 1st ` c ) e. _V |
8 |
|
breq1 |
|- ( f = ( 1st ` c ) -> ( f ( ClWalks ` G ) ( 2nd ` c ) <-> ( 1st ` c ) ( ClWalks ` G ) ( 2nd ` c ) ) ) |
9 |
7 8
|
spcev |
|- ( ( 1st ` c ) ( ClWalks ` G ) ( 2nd ` c ) -> E. f f ( ClWalks ` G ) ( 2nd ` c ) ) |
10 |
6 9
|
sylbir |
|- ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) ) -> E. f f ( ClWalks ` G ) ( 2nd ` c ) ) |
11 |
10
|
3adant3 |
|- ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) e. NN ) -> E. f f ( ClWalks ` G ) ( 2nd ` c ) ) |
12 |
11
|
adantl |
|- ( ( G e. USPGraph /\ ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) e. NN ) ) -> E. f f ( ClWalks ` G ) ( 2nd ` c ) ) |
13 |
|
simpl |
|- ( ( G e. USPGraph /\ ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) e. NN ) ) -> G e. USPGraph ) |
14 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
15 |
14
|
wlkpwrd |
|- ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( 2nd ` c ) e. Word ( Vtx ` G ) ) |
16 |
15
|
3ad2ant1 |
|- ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) e. NN ) -> ( 2nd ` c ) e. Word ( Vtx ` G ) ) |
17 |
16
|
adantl |
|- ( ( G e. USPGraph /\ ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) e. NN ) ) -> ( 2nd ` c ) e. Word ( Vtx ` G ) ) |
18 |
|
elnnnn0c |
|- ( ( # ` ( 1st ` c ) ) e. NN <-> ( ( # ` ( 1st ` c ) ) e. NN0 /\ 1 <_ ( # ` ( 1st ` c ) ) ) ) |
19 |
|
nn0re |
|- ( ( # ` ( 1st ` c ) ) e. NN0 -> ( # ` ( 1st ` c ) ) e. RR ) |
20 |
|
1e2m1 |
|- 1 = ( 2 - 1 ) |
21 |
20
|
breq1i |
|- ( 1 <_ ( # ` ( 1st ` c ) ) <-> ( 2 - 1 ) <_ ( # ` ( 1st ` c ) ) ) |
22 |
21
|
biimpi |
|- ( 1 <_ ( # ` ( 1st ` c ) ) -> ( 2 - 1 ) <_ ( # ` ( 1st ` c ) ) ) |
23 |
|
2re |
|- 2 e. RR |
24 |
|
1re |
|- 1 e. RR |
25 |
|
lesubadd |
|- ( ( 2 e. RR /\ 1 e. RR /\ ( # ` ( 1st ` c ) ) e. RR ) -> ( ( 2 - 1 ) <_ ( # ` ( 1st ` c ) ) <-> 2 <_ ( ( # ` ( 1st ` c ) ) + 1 ) ) ) |
26 |
23 24 25
|
mp3an12 |
|- ( ( # ` ( 1st ` c ) ) e. RR -> ( ( 2 - 1 ) <_ ( # ` ( 1st ` c ) ) <-> 2 <_ ( ( # ` ( 1st ` c ) ) + 1 ) ) ) |
27 |
22 26
|
syl5ib |
|- ( ( # ` ( 1st ` c ) ) e. RR -> ( 1 <_ ( # ` ( 1st ` c ) ) -> 2 <_ ( ( # ` ( 1st ` c ) ) + 1 ) ) ) |
28 |
19 27
|
syl |
|- ( ( # ` ( 1st ` c ) ) e. NN0 -> ( 1 <_ ( # ` ( 1st ` c ) ) -> 2 <_ ( ( # ` ( 1st ` c ) ) + 1 ) ) ) |
29 |
28
|
adantl |
|- ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( # ` ( 1st ` c ) ) e. NN0 ) -> ( 1 <_ ( # ` ( 1st ` c ) ) -> 2 <_ ( ( # ` ( 1st ` c ) ) + 1 ) ) ) |
30 |
|
wlklenvp1 |
|- ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( # ` ( 2nd ` c ) ) = ( ( # ` ( 1st ` c ) ) + 1 ) ) |
31 |
30
|
adantr |
|- ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( # ` ( 1st ` c ) ) e. NN0 ) -> ( # ` ( 2nd ` c ) ) = ( ( # ` ( 1st ` c ) ) + 1 ) ) |
32 |
31
|
breq2d |
|- ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( # ` ( 1st ` c ) ) e. NN0 ) -> ( 2 <_ ( # ` ( 2nd ` c ) ) <-> 2 <_ ( ( # ` ( 1st ` c ) ) + 1 ) ) ) |
33 |
29 32
|
sylibrd |
|- ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( # ` ( 1st ` c ) ) e. NN0 ) -> ( 1 <_ ( # ` ( 1st ` c ) ) -> 2 <_ ( # ` ( 2nd ` c ) ) ) ) |
34 |
33
|
expimpd |
|- ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( ( ( # ` ( 1st ` c ) ) e. NN0 /\ 1 <_ ( # ` ( 1st ` c ) ) ) -> 2 <_ ( # ` ( 2nd ` c ) ) ) ) |
35 |
18 34
|
syl5bi |
|- ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( ( # ` ( 1st ` c ) ) e. NN -> 2 <_ ( # ` ( 2nd ` c ) ) ) ) |
36 |
35
|
a1d |
|- ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) -> ( ( # ` ( 1st ` c ) ) e. NN -> 2 <_ ( # ` ( 2nd ` c ) ) ) ) ) |
37 |
36
|
3imp |
|- ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) e. NN ) -> 2 <_ ( # ` ( 2nd ` c ) ) ) |
38 |
37
|
adantl |
|- ( ( G e. USPGraph /\ ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) e. NN ) ) -> 2 <_ ( # ` ( 2nd ` c ) ) ) |
39 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
40 |
14 39
|
clwlkclwwlk |
|- ( ( G e. USPGraph /\ ( 2nd ` c ) e. Word ( Vtx ` G ) /\ 2 <_ ( # ` ( 2nd ` c ) ) ) -> ( E. f f ( ClWalks ` G ) ( 2nd ` c ) <-> ( ( lastS ` ( 2nd ` c ) ) = ( ( 2nd ` c ) ` 0 ) /\ ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) e. ( ClWWalks ` G ) ) ) ) |
41 |
13 17 38 40
|
syl3anc |
|- ( ( G e. USPGraph /\ ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) e. NN ) ) -> ( E. f f ( ClWalks ` G ) ( 2nd ` c ) <-> ( ( lastS ` ( 2nd ` c ) ) = ( ( 2nd ` c ) ` 0 ) /\ ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) e. ( ClWWalks ` G ) ) ) ) |
42 |
12 41
|
mpbid |
|- ( ( G e. USPGraph /\ ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( ( 2nd ` c ) ` 0 ) = ( ( 2nd ` c ) ` ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) e. NN ) ) -> ( ( lastS ` ( 2nd ` c ) ) = ( ( 2nd ` c ) ` 0 ) /\ ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) e. ( ClWWalks ` G ) ) ) |
43 |
5 42
|
sylan2 |
|- ( ( G e. USPGraph /\ c e. C ) -> ( ( lastS ` ( 2nd ` c ) ) = ( ( 2nd ` c ) ` 0 ) /\ ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) e. ( ClWWalks ` G ) ) ) |
44 |
43
|
simprd |
|- ( ( G e. USPGraph /\ c e. C ) -> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) e. ( ClWWalks ` G ) ) |
45 |
44 2
|
fmptd |
|- ( G e. USPGraph -> F : C --> ( ClWWalks ` G ) ) |