Metamath Proof Explorer

Theorem clwlkclwwlkfo

Description: F is a function from the nonempty closed walks onto the closed walks as words in a simple pseudograph. (Contributed by Alexander van der Vekens, 30-Jun-2018) (Revised by AV, 2-May-2021) (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 clwlkclwwlkfo 
|- ( G e. USPGraph -> F : C -onto-> ( 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 1 2 clwlkclwwlkf 
 |-  ( G e. USPGraph -> F : C --> ( ClWWalks ` G ) )
4 clwwlkgt0 
 |-  ( w e. ( ClWWalks ` G ) -> 0 < ( # ` w ) )
5 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
6 5 clwwlkbp 
 |-  ( w e. ( ClWWalks ` G ) -> ( G e. _V /\ w e. Word ( Vtx ` G ) /\ w =/= (/) ) )
7 lencl 
 |-  ( w e. Word ( Vtx ` G ) -> ( # ` w ) e. NN0 )
8 7 nn0zd 
 |-  ( w e. Word ( Vtx ` G ) -> ( # ` w ) e. ZZ )
9 zgt0ge1 
 |-  ( ( # ` w ) e. ZZ -> ( 0 < ( # ` w ) <-> 1 <_ ( # ` w ) ) )
10 8 9 syl 
 |-  ( w e. Word ( Vtx ` G ) -> ( 0 < ( # ` w ) <-> 1 <_ ( # ` w ) ) )
11 10 biimpd 
 |-  ( w e. Word ( Vtx ` G ) -> ( 0 < ( # ` w ) -> 1 <_ ( # ` w ) ) )
12 11 anc2li 
 |-  ( w e. Word ( Vtx ` G ) -> ( 0 < ( # ` w ) -> ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) ) )
13 12 3ad2ant2 
 |-  ( ( G e. _V /\ w e. Word ( Vtx ` G ) /\ w =/= (/) ) -> ( 0 < ( # ` w ) -> ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) ) )
14 6 13 syl 
 |-  ( w e. ( ClWWalks ` G ) -> ( 0 < ( # ` w ) -> ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) ) )
15 4 14 mpd 
 |-  ( w e. ( ClWWalks ` G ) -> ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) )
16 15 adantl 
 |-  ( ( G e. USPGraph /\ w e. ( ClWWalks ` G ) ) -> ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) )
17 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
18 5 17 clwlkclwwlk2 
 |-  ( ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> ( E. f f ( ClWalks ` G ) ( w ++ <" ( w ` 0 ) "> ) <-> w e. ( ClWWalks ` G ) ) )
19 df-br 
 |-  ( f ( ClWalks ` G ) ( w ++ <" ( w ` 0 ) "> ) <-> <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) )
20 simpr2 
 |-  ( ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) /\ ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) ) -> w e. Word ( Vtx ` G ) )
21 simpr3 
 |-  ( ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) /\ ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) ) -> 1 <_ ( # ` w ) )
22 simpl 
 |-  ( ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) /\ ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) ) -> <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) )
23 1 clwlkclwwlkfolem 
 |-  ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. C )
24 20 21 22 23 syl3anc 
 |-  ( ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) /\ ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) ) -> <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. C )
25 23 3expa 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. C )
26 ovex 
 |-  ( ( w ++ <" ( w ` 0 ) "> ) prefix ( ( # ` ( w ++ <" ( w ` 0 ) "> ) ) - 1 ) ) e. _V
27 fveq2 
 |-  ( c = <. f , ( w ++ <" ( w ` 0 ) "> ) >. -> ( 2nd ` c ) = ( 2nd ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) )
28 2fveq3 
 |-  ( c = <. f , ( w ++ <" ( w ` 0 ) "> ) >. -> ( # ` ( 2nd ` c ) ) = ( # ` ( 2nd ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) )
29 28 oveq1d 
 |-  ( c = <. f , ( w ++ <" ( w ` 0 ) "> ) >. -> ( ( # ` ( 2nd ` c ) ) - 1 ) = ( ( # ` ( 2nd ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) - 1 ) )
30 27 29 oveq12d 
 |-  ( c = <. f , ( w ++ <" ( w ` 0 ) "> ) >. -> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) = ( ( 2nd ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) prefix ( ( # ` ( 2nd ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) - 1 ) ) )
31 vex 
 |-  f e. _V
32 ovex 
 |-  ( w ++ <" ( w ` 0 ) "> ) e. _V
33 31 32 op2nd 
 |-  ( 2nd ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) = ( w ++ <" ( w ` 0 ) "> )
34 33 fveq2i 
 |-  ( # ` ( 2nd ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) = ( # ` ( w ++ <" ( w ` 0 ) "> ) )
35 34 oveq1i 
 |-  ( ( # ` ( 2nd ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) - 1 ) = ( ( # ` ( w ++ <" ( w ` 0 ) "> ) ) - 1 )
36 33 35 oveq12i 
 |-  ( ( 2nd ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) prefix ( ( # ` ( 2nd ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) - 1 ) ) = ( ( w ++ <" ( w ` 0 ) "> ) prefix ( ( # ` ( w ++ <" ( w ` 0 ) "> ) ) - 1 ) )
37 30 36 eqtrdi 
 |-  ( c = <. f , ( w ++ <" ( w ` 0 ) "> ) >. -> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) = ( ( w ++ <" ( w ` 0 ) "> ) prefix ( ( # ` ( w ++ <" ( w ` 0 ) "> ) ) - 1 ) ) )
38 37 2 fvmptg 
 |-  ( ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. C /\ ( ( w ++ <" ( w ` 0 ) "> ) prefix ( ( # ` ( w ++ <" ( w ` 0 ) "> ) ) - 1 ) ) e. _V ) -> ( F ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) = ( ( w ++ <" ( w ` 0 ) "> ) prefix ( ( # ` ( w ++ <" ( w ` 0 ) "> ) ) - 1 ) ) )
39 25 26 38 sylancl 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> ( F ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) = ( ( w ++ <" ( w ` 0 ) "> ) prefix ( ( # ` ( w ++ <" ( w ` 0 ) "> ) ) - 1 ) ) )
40 wrdlenccats1lenm1 
 |-  ( w e. Word ( Vtx ` G ) -> ( ( # ` ( w ++ <" ( w ` 0 ) "> ) ) - 1 ) = ( # ` w ) )
41 40 ad2antrr 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> ( ( # ` ( w ++ <" ( w ` 0 ) "> ) ) - 1 ) = ( # ` w ) )
42 41 oveq2d 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> ( ( w ++ <" ( w ` 0 ) "> ) prefix ( ( # ` ( w ++ <" ( w ` 0 ) "> ) ) - 1 ) ) = ( ( w ++ <" ( w ` 0 ) "> ) prefix ( # ` w ) ) )
43 simpll 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> w e. Word ( Vtx ` G ) )
44 simpl 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) )
45 wrdsymb1 
 |-  ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> ( w ` 0 ) e. ( Vtx ` G ) )
46 44 45 syl 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> ( w ` 0 ) e. ( Vtx ` G ) )
47 46 s1cld 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> <" ( w ` 0 ) "> e. Word ( Vtx ` G ) )
48 eqidd 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> ( # ` w ) = ( # ` w ) )
49 pfxccatid 
 |-  ( ( w e. Word ( Vtx ` G ) /\ <" ( w ` 0 ) "> e. Word ( Vtx ` G ) /\ ( # ` w ) = ( # ` w ) ) -> ( ( w ++ <" ( w ` 0 ) "> ) prefix ( # ` w ) ) = w )
50 43 47 48 49 syl3anc 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> ( ( w ++ <" ( w ` 0 ) "> ) prefix ( # ` w ) ) = w )
51 39 42 50 3eqtrrd 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) /\ <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> w = ( F ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) )
52 51 ex 
 |-  ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> w = ( F ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) )
53 52 3adant1 
 |-  ( ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> w = ( F ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) )
54 53 ad2antlr 
 |-  ( ( ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) /\ ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) ) /\ c = <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) -> ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> w = ( F ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) )
55 fveq2 
 |-  ( c = <. f , ( w ++ <" ( w ` 0 ) "> ) >. -> ( F ` c ) = ( F ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) )
56 55 eqeq2d 
 |-  ( c = <. f , ( w ++ <" ( w ` 0 ) "> ) >. -> ( w = ( F ` c ) <-> w = ( F ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) )
57 56 imbi2d 
 |-  ( c = <. f , ( w ++ <" ( w ` 0 ) "> ) >. -> ( ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> w = ( F ` c ) ) <-> ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> w = ( F ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) ) )
58 57 adantl 
 |-  ( ( ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) /\ ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) ) /\ c = <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) -> ( ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> w = ( F ` c ) ) <-> ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> w = ( F ` <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) ) ) )
59 54 58 mpbird 
 |-  ( ( ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) /\ ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) ) /\ c = <. f , ( w ++ <" ( w ` 0 ) "> ) >. ) -> ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> w = ( F ` c ) ) )
60 24 59 rspcimedv 
 |-  ( ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) /\ ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) ) -> ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> E. c e. C w = ( F ` c ) ) )
61 60 ex 
 |-  ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> ( ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> E. c e. C w = ( F ` c ) ) ) )
62 61 pm2.43b 
 |-  ( ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> ( <. f , ( w ++ <" ( w ` 0 ) "> ) >. e. ( ClWalks ` G ) -> E. c e. C w = ( F ` c ) ) )
63 19 62 biimtrid 
 |-  ( ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> ( f ( ClWalks ` G ) ( w ++ <" ( w ` 0 ) "> ) -> E. c e. C w = ( F ` c ) ) )
64 63 exlimdv 
 |-  ( ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> ( E. f f ( ClWalks ` G ) ( w ++ <" ( w ` 0 ) "> ) -> E. c e. C w = ( F ` c ) ) )
65 18 64 sylbird 
 |-  ( ( G e. USPGraph /\ w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> ( w e. ( ClWWalks ` G ) -> E. c e. C w = ( F ` c ) ) )
66 65 3expib 
 |-  ( G e. USPGraph -> ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> ( w e. ( ClWWalks ` G ) -> E. c e. C w = ( F ` c ) ) ) )
67 66 com23 
 |-  ( G e. USPGraph -> ( w e. ( ClWWalks ` G ) -> ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> E. c e. C w = ( F ` c ) ) ) )
68 67 imp 
 |-  ( ( G e. USPGraph /\ w e. ( ClWWalks ` G ) ) -> ( ( w e. Word ( Vtx ` G ) /\ 1 <_ ( # ` w ) ) -> E. c e. C w = ( F ` c ) ) )
69 16 68 mpd 
 |-  ( ( G e. USPGraph /\ w e. ( ClWWalks ` G ) ) -> E. c e. C w = ( F ` c ) )
70 69 ralrimiva 
 |-  ( G e. USPGraph -> A. w e. ( ClWWalks ` G ) E. c e. C w = ( F ` c ) )
71 dffo3 
 |-  ( F : C -onto-> ( ClWWalks ` G ) <-> ( F : C --> ( ClWWalks ` G ) /\ A. w e. ( ClWWalks ` G ) E. c e. C w = ( F ` c ) ) )
72 3 70 71 sylanbrc 
 |-  ( G e. USPGraph -> F : C -onto-> ( ClWWalks ` G ) )