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 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 ) )