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 ClWalks G | 1 1 st w
clwlkclwwlkf.f F = c C 2 nd c prefix 2 nd c 1
Assertion clwlkclwwlkfo G USHGraph F : C onto ClWWalks G

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c C = w ClWalks G | 1 1 st w
2 clwlkclwwlkf.f F = c C 2 nd c prefix 2 nd c 1
3 1 2 clwlkclwwlkf G USHGraph F : C ClWWalks G
4 clwwlkgt0 w ClWWalks G 0 < w
5 eqid Vtx G = Vtx G
6 5 clwwlkbp w ClWWalks G G V w Word Vtx G w
7 lencl w Word Vtx G w 0
8 7 nn0zd w Word Vtx G w
9 zgt0ge1 w 0 < w 1 w
10 8 9 syl w Word Vtx G 0 < w 1 w
11 10 biimpd w Word Vtx G 0 < w 1 w
12 11 anc2li w Word Vtx G 0 < w w Word Vtx G 1 w
13 12 3ad2ant2 G V w Word Vtx G w 0 < w w Word Vtx G 1 w
14 6 13 syl w ClWWalks G 0 < w w Word Vtx G 1 w
15 4 14 mpd w ClWWalks G w Word Vtx G 1 w
16 15 adantl G USHGraph w ClWWalks G w Word Vtx G 1 w
17 eqid iEdg G = iEdg G
18 5 17 clwlkclwwlk2 G USHGraph w Word Vtx G 1 w f f ClWalks G w ++ ⟨“ w 0 ”⟩ w ClWWalks G
19 df-br f ClWalks G w ++ ⟨“ w 0 ”⟩ f w ++ ⟨“ w 0 ”⟩ ClWalks G
20 simpr2 f w ++ ⟨“ w 0 ”⟩ ClWalks G G USHGraph w Word Vtx G 1 w w Word Vtx G
21 simpr3 f w ++ ⟨“ w 0 ”⟩ ClWalks G G USHGraph w Word Vtx G 1 w 1 w
22 simpl f w ++ ⟨“ w 0 ”⟩ ClWalks G G USHGraph w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G
23 1 clwlkclwwlkfolem w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G f w ++ ⟨“ w 0 ”⟩ C
24 20 21 22 23 syl3anc f w ++ ⟨“ w 0 ”⟩ ClWalks G G USHGraph w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ C
25 23 3expa w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G f w ++ ⟨“ w 0 ”⟩ C
26 ovex w ++ ⟨“ w 0 ”⟩ prefix w ++ ⟨“ w 0 ”⟩ 1 V
27 fveq2 c = f w ++ ⟨“ w 0 ”⟩ 2 nd c = 2 nd f w ++ ⟨“ w 0 ”⟩
28 2fveq3 c = f w ++ ⟨“ w 0 ”⟩ 2 nd c = 2 nd f w ++ ⟨“ w 0 ”⟩
29 28 oveq1d c = f w ++ ⟨“ w 0 ”⟩ 2 nd c 1 = 2 nd f w ++ ⟨“ w 0 ”⟩ 1
30 27 29 oveq12d c = f w ++ ⟨“ w 0 ”⟩ 2 nd c prefix 2 nd c 1 = 2 nd f w ++ ⟨“ w 0 ”⟩ prefix 2 nd f w ++ ⟨“ w 0 ”⟩ 1
31 vex f V
32 ovex w ++ ⟨“ w 0 ”⟩ V
33 31 32 op2nd 2 nd f w ++ ⟨“ w 0 ”⟩ = w ++ ⟨“ w 0 ”⟩
34 33 fveq2i 2 nd f w ++ ⟨“ w 0 ”⟩ = w ++ ⟨“ w 0 ”⟩
35 34 oveq1i 2 nd f w ++ ⟨“ w 0 ”⟩ 1 = w ++ ⟨“ w 0 ”⟩ 1
36 33 35 oveq12i 2 nd f w ++ ⟨“ w 0 ”⟩ prefix 2 nd f w ++ ⟨“ w 0 ”⟩ 1 = w ++ ⟨“ w 0 ”⟩ prefix w ++ ⟨“ w 0 ”⟩ 1
37 30 36 syl6eq c = f w ++ ⟨“ w 0 ”⟩ 2 nd c prefix 2 nd c 1 = w ++ ⟨“ w 0 ”⟩ prefix w ++ ⟨“ w 0 ”⟩ 1
38 37 2 fvmptg f w ++ ⟨“ w 0 ”⟩ C w ++ ⟨“ w 0 ”⟩ prefix w ++ ⟨“ w 0 ”⟩ 1 V F f w ++ ⟨“ w 0 ”⟩ = w ++ ⟨“ w 0 ”⟩ prefix w ++ ⟨“ w 0 ”⟩ 1
39 25 26 38 sylancl w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G F f w ++ ⟨“ w 0 ”⟩ = w ++ ⟨“ w 0 ”⟩ prefix w ++ ⟨“ w 0 ”⟩ 1
40 wrdlenccats1lenm1 w Word Vtx G w ++ ⟨“ w 0 ”⟩ 1 = w
41 40 ad2antrr w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G w ++ ⟨“ w 0 ”⟩ 1 = w
42 41 oveq2d w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G w ++ ⟨“ w 0 ”⟩ prefix w ++ ⟨“ w 0 ”⟩ 1 = w ++ ⟨“ w 0 ”⟩ prefix w
43 simpll w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G w Word Vtx G
44 simpl w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G w Word Vtx G 1 w
45 wrdsymb1 w Word Vtx G 1 w w 0 Vtx G
46 44 45 syl w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G w 0 Vtx G
47 46 s1cld w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G ⟨“ w 0 ”⟩ Word Vtx G
48 eqidd w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G w = w
49 pfxccatid w Word Vtx G ⟨“ w 0 ”⟩ Word Vtx G w = w w ++ ⟨“ w 0 ”⟩ prefix w = w
50 43 47 48 49 syl3anc w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G w ++ ⟨“ w 0 ”⟩ prefix w = w
51 39 42 50 3eqtrrd w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G w = F f w ++ ⟨“ w 0 ”⟩
52 51 ex w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G w = F f w ++ ⟨“ w 0 ”⟩
53 52 3adant1 G USHGraph w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G w = F f w ++ ⟨“ w 0 ”⟩
54 53 ad2antlr f w ++ ⟨“ w 0 ”⟩ ClWalks G G USHGraph w Word Vtx G 1 w c = f w ++ ⟨“ w 0 ”⟩ f w ++ ⟨“ w 0 ”⟩ 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 ”⟩ ClWalks G w = F c f w ++ ⟨“ w 0 ”⟩ ClWalks G w = F f w ++ ⟨“ w 0 ”⟩
58 57 adantl f w ++ ⟨“ w 0 ”⟩ ClWalks G G USHGraph w Word Vtx G 1 w c = f w ++ ⟨“ w 0 ”⟩ f w ++ ⟨“ w 0 ”⟩ ClWalks G w = F c f w ++ ⟨“ w 0 ”⟩ ClWalks G w = F f w ++ ⟨“ w 0 ”⟩
59 54 58 mpbird f w ++ ⟨“ w 0 ”⟩ ClWalks G G USHGraph w Word Vtx G 1 w c = f w ++ ⟨“ w 0 ”⟩ f w ++ ⟨“ w 0 ”⟩ ClWalks G w = F c
60 24 59 rspcimedv f w ++ ⟨“ w 0 ”⟩ ClWalks G G USHGraph w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G c C w = F c
61 60 ex f w ++ ⟨“ w 0 ”⟩ ClWalks G G USHGraph w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G c C w = F c
62 61 pm2.43b G USHGraph w Word Vtx G 1 w f w ++ ⟨“ w 0 ”⟩ ClWalks G c C w = F c
63 19 62 syl5bi G USHGraph w Word Vtx G 1 w f ClWalks G w ++ ⟨“ w 0 ”⟩ c C w = F c
64 63 exlimdv G USHGraph w Word Vtx G 1 w f f ClWalks G w ++ ⟨“ w 0 ”⟩ c C w = F c
65 18 64 sylbird G USHGraph w Word Vtx G 1 w w ClWWalks G c C w = F c
66 65 3expib G USHGraph w Word Vtx G 1 w w ClWWalks G c C w = F c
67 66 com23 G USHGraph w ClWWalks G w Word Vtx G 1 w c C w = F c
68 67 imp G USHGraph w ClWWalks G w Word Vtx G 1 w c C w = F c
69 16 68 mpd G USHGraph w ClWWalks G c C w = F c
70 69 ralrimiva G USHGraph w ClWWalks G c C w = F c
71 dffo3 F : C onto ClWWalks G F : C ClWWalks G w ClWWalks G c C w = F c
72 3 70 71 sylanbrc G USHGraph F : C onto ClWWalks G