Metamath Proof Explorer

Theorem clwlkclwwlkf

Description: F is a function from the nonempty closed walks into the closed walks as word in a simple pseudograph. (Contributed by AV, 23-May-2022) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlkf.c 
|- C = { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) }
clwlkclwwlkf.f 
|- F = ( c e. C |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
Assertion clwlkclwwlkf 
|- ( G e. USPGraph -> F : C --> ( ClWWalks ` G ) )

Proof

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 imbitrid 
 |-  ( ( # ` ( 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 biimtrid 
 |-  ( ( 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 ) )