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 eqtrdi ⊢ 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