Metamath Proof Explorer

Theorem clwlknf1oclwwlkn

Description: There is a one-to-one onto function between the set of closed walks as words of length N and the set of closed walks of length N in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018) (Revised by AV, 3-May-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwlknf1oclwwlkn.a ⊢ A = 1 st ⁡ c
clwlknf1oclwwlkn.b ⊢ B = 2 nd ⁡ c
clwlknf1oclwwlkn.c ⊢ C = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N
clwlknf1oclwwlkn.f ⊢ F = c ∈ C ⟼ B prefix A
Assertion clwlknf1oclwwlkn ⊢ G ∈ USHGraph ∧ N ∈ ℕ → F : C ⟶ 1-1 onto N ClWWalksN G

Proof

Step Hyp Ref Expression
1 clwlknf1oclwwlkn.a ⊢ A = 1 st ⁡ c
2 clwlknf1oclwwlkn.b ⊢ B = 2 nd ⁡ c
3 clwlknf1oclwwlkn.c ⊢ C = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N
4 clwlknf1oclwwlkn.f ⊢ F = c ∈ C ⟼ B prefix A
5 eqid ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1 = c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1
6 2fveq3 ⊢ s = w → 1 st ⁡ s = 1 st ⁡ w
7 6 breq2d ⊢ s = w → 1 ≤ 1 st ⁡ s ↔ 1 ≤ 1 st ⁡ w
8 7 cbvrabv ⊢ s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s = w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w
9 fveq2 ⊢ d = c → 2 nd ⁡ d = 2 nd ⁡ c
10 2fveq3 ⊢ d = c → 2 nd ⁡ d = 2 nd ⁡ c
11 10 oveq1d ⊢ d = c → 2 nd ⁡ d − 1 = 2 nd ⁡ c − 1
12 9 11 oveq12d ⊢ d = c → 2 nd ⁡ d prefix 2 nd ⁡ d − 1 = 2 nd ⁡ c prefix 2 nd ⁡ c − 1
13 12 cbvmptv ⊢ d ∈ s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟼ 2 nd ⁡ d prefix 2 nd ⁡ d − 1 = c ∈ s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1
14 8 13 clwlkclwwlkf1o ⊢ G ∈ USHGraph → d ∈ s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟼ 2 nd ⁡ d prefix 2 nd ⁡ d − 1 : s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟶ 1-1 onto ClWWalks ⁡ G
15 14 adantr ⊢ G ∈ USHGraph ∧ N ∈ ℕ → d ∈ s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟼ 2 nd ⁡ d prefix 2 nd ⁡ d − 1 : s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟶ 1-1 onto ClWWalks ⁡ G
16 2fveq3 ⊢ w = s → 1 st ⁡ w = 1 st ⁡ s
17 16 breq2d ⊢ w = s → 1 ≤ 1 st ⁡ w ↔ 1 ≤ 1 st ⁡ s
18 17 cbvrabv ⊢ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w = s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s
19 18 mpteq1i ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1 = c ∈ s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1
20 fveq2 ⊢ c = d → 2 nd ⁡ c = 2 nd ⁡ d
21 2fveq3 ⊢ c = d → 2 nd ⁡ c = 2 nd ⁡ d
22 21 oveq1d ⊢ c = d → 2 nd ⁡ c − 1 = 2 nd ⁡ d − 1
23 20 22 oveq12d ⊢ c = d → 2 nd ⁡ c prefix 2 nd ⁡ c − 1 = 2 nd ⁡ d prefix 2 nd ⁡ d − 1
24 23 cbvmptv ⊢ c ∈ s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1 = d ∈ s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟼ 2 nd ⁡ d prefix 2 nd ⁡ d − 1
25 19 24 eqtri ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1 = d ∈ s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟼ 2 nd ⁡ d prefix 2 nd ⁡ d − 1
26 25 a1i ⊢ G ∈ USHGraph ∧ N ∈ ℕ → c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1 = d ∈ s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟼ 2 nd ⁡ d prefix 2 nd ⁡ d − 1
27 8 eqcomi ⊢ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w = s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s
28 27 a1i ⊢ G ∈ USHGraph ∧ N ∈ ℕ → w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w = s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s
29 eqidd ⊢ G ∈ USHGraph ∧ N ∈ ℕ → ClWWalks ⁡ G = ClWWalks ⁡ G
30 26 28 29 f1oeq123d ⊢ G ∈ USHGraph ∧ N ∈ ℕ → c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1 : w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟶ 1-1 onto ClWWalks ⁡ G ↔ d ∈ s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟼ 2 nd ⁡ d prefix 2 nd ⁡ d − 1 : s ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ s ⟶ 1-1 onto ClWWalks ⁡ G
31 15 30 mpbird ⊢ G ∈ USHGraph ∧ N ∈ ℕ → c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1 : w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟶ 1-1 onto ClWWalks ⁡ G
32 fveq2 ⊢ s = 2 nd ⁡ c prefix 2 nd ⁡ c − 1 → s = 2 nd ⁡ c prefix 2 nd ⁡ c − 1
33 32 3ad2ant3 ⊢ G ∈ USHGraph ∧ N ∈ ℕ ∧ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ∧ s = 2 nd ⁡ c prefix 2 nd ⁡ c − 1 → s = 2 nd ⁡ c prefix 2 nd ⁡ c − 1
34 2fveq3 ⊢ w = c → 1 st ⁡ w = 1 st ⁡ c
35 34 breq2d ⊢ w = c → 1 ≤ 1 st ⁡ w ↔ 1 ≤ 1 st ⁡ c
36 35 elrab ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ↔ c ∈ ClWalks ⁡ G ∧ 1 ≤ 1 st ⁡ c
37 clwlknf1oclwwlknlem1 ⊢ c ∈ ClWalks ⁡ G ∧ 1 ≤ 1 st ⁡ c → 2 nd ⁡ c prefix 2 nd ⁡ c − 1 = 1 st ⁡ c
38 36 37 sylbi ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w → 2 nd ⁡ c prefix 2 nd ⁡ c − 1 = 1 st ⁡ c
39 38 3ad2ant2 ⊢ G ∈ USHGraph ∧ N ∈ ℕ ∧ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ∧ s = 2 nd ⁡ c prefix 2 nd ⁡ c − 1 → 2 nd ⁡ c prefix 2 nd ⁡ c − 1 = 1 st ⁡ c
40 33 39 eqtrd ⊢ G ∈ USHGraph ∧ N ∈ ℕ ∧ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ∧ s = 2 nd ⁡ c prefix 2 nd ⁡ c − 1 → s = 1 st ⁡ c
41 40 eqeq1d ⊢ G ∈ USHGraph ∧ N ∈ ℕ ∧ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ∧ s = 2 nd ⁡ c prefix 2 nd ⁡ c − 1 → s = N ↔ 1 st ⁡ c = N
42 5 31 41 f1oresrab ⊢ G ∈ USHGraph ∧ N ∈ ℕ → c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1 ↾ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w | 1 st ⁡ c = N : c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w | 1 st ⁡ c = N ⟶ 1-1 onto s ∈ ClWWalks ⁡ G | s = N
43 1 2 3 4 clwlknf1oclwwlknlem3 ⊢ G ∈ USHGraph ∧ N ∈ ℕ → F = c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ B prefix A ↾ C
44 2 a1i ⊢ G ∈ USHGraph ∧ N ∈ ℕ ∧ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w → B = 2 nd ⁡ c
45 clwlkwlk ⊢ c ∈ ClWalks ⁡ G → c ∈ Walks ⁡ G
46 wlkcpr ⊢ c ∈ Walks ⁡ G ↔ 1 st ⁡ c Walks ⁡ G 2 nd ⁡ c
47 1 fveq2i ⊢ A = 1 st ⁡ c
48 wlklenvm1 ⊢ 1 st ⁡ c Walks ⁡ G 2 nd ⁡ c → 1 st ⁡ c = 2 nd ⁡ c − 1
49 47 48 syl5eq ⊢ 1 st ⁡ c Walks ⁡ G 2 nd ⁡ c → A = 2 nd ⁡ c − 1
50 46 49 sylbi ⊢ c ∈ Walks ⁡ G → A = 2 nd ⁡ c − 1
51 45 50 syl ⊢ c ∈ ClWalks ⁡ G → A = 2 nd ⁡ c − 1
52 51 adantr ⊢ c ∈ ClWalks ⁡ G ∧ 1 ≤ 1 st ⁡ c → A = 2 nd ⁡ c − 1
53 36 52 sylbi ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w → A = 2 nd ⁡ c − 1
54 53 adantl ⊢ G ∈ USHGraph ∧ N ∈ ℕ ∧ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w → A = 2 nd ⁡ c − 1
55 44 54 oveq12d ⊢ G ∈ USHGraph ∧ N ∈ ℕ ∧ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w → B prefix A = 2 nd ⁡ c prefix 2 nd ⁡ c − 1
56 55 mpteq2dva ⊢ G ∈ USHGraph ∧ N ∈ ℕ → c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ B prefix A = c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1
57 34 eqeq1d ⊢ w = c → 1 st ⁡ w = N ↔ 1 st ⁡ c = N
58 57 cbvrabv ⊢ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N = c ∈ ClWalks ⁡ G | 1 st ⁡ c = N
59 nnge1 ⊢ N ∈ ℕ → 1 ≤ N
60 breq2 ⊢ 1 st ⁡ c = N → 1 ≤ 1 st ⁡ c ↔ 1 ≤ N
61 59 60 syl5ibrcom ⊢ N ∈ ℕ → 1 st ⁡ c = N → 1 ≤ 1 st ⁡ c
62 61 adantl ⊢ G ∈ USHGraph ∧ N ∈ ℕ → 1 st ⁡ c = N → 1 ≤ 1 st ⁡ c
63 62 adantr ⊢ G ∈ USHGraph ∧ N ∈ ℕ ∧ c ∈ ClWalks ⁡ G → 1 st ⁡ c = N → 1 ≤ 1 st ⁡ c
64 63 pm4.71rd ⊢ G ∈ USHGraph ∧ N ∈ ℕ ∧ c ∈ ClWalks ⁡ G → 1 st ⁡ c = N ↔ 1 ≤ 1 st ⁡ c ∧ 1 st ⁡ c = N
65 64 rabbidva ⊢ G ∈ USHGraph ∧ N ∈ ℕ → c ∈ ClWalks ⁡ G | 1 st ⁡ c = N = c ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ c ∧ 1 st ⁡ c = N
66 58 65 syl5eq ⊢ G ∈ USHGraph ∧ N ∈ ℕ → w ∈ ClWalks ⁡ G | 1 st ⁡ w = N = c ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ c ∧ 1 st ⁡ c = N
67 36 anbi1i ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ∧ 1 st ⁡ c = N ↔ c ∈ ClWalks ⁡ G ∧ 1 ≤ 1 st ⁡ c ∧ 1 st ⁡ c = N
68 anass ⊢ c ∈ ClWalks ⁡ G ∧ 1 ≤ 1 st ⁡ c ∧ 1 st ⁡ c = N ↔ c ∈ ClWalks ⁡ G ∧ 1 ≤ 1 st ⁡ c ∧ 1 st ⁡ c = N
69 67 68 bitri ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ∧ 1 st ⁡ c = N ↔ c ∈ ClWalks ⁡ G ∧ 1 ≤ 1 st ⁡ c ∧ 1 st ⁡ c = N
70 69 rabbia2 ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w | 1 st ⁡ c = N = c ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ c ∧ 1 st ⁡ c = N
71 66 3 70 3eqtr4g ⊢ G ∈ USHGraph ∧ N ∈ ℕ → C = c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w | 1 st ⁡ c = N
72 56 71 reseq12d ⊢ G ∈ USHGraph ∧ N ∈ ℕ → c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ B prefix A ↾ C = c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1 ↾ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w | 1 st ⁡ c = N
73 43 72 eqtrd ⊢ G ∈ USHGraph ∧ N ∈ ℕ → F = c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1 ↾ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w | 1 st ⁡ c = N
74 clwlknf1oclwwlknlem2 ⊢ N ∈ ℕ → w ∈ ClWalks ⁡ G | 1 st ⁡ w = N = c ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ c ∧ 1 st ⁡ c = N
75 74 adantl ⊢ G ∈ USHGraph ∧ N ∈ ℕ → w ∈ ClWalks ⁡ G | 1 st ⁡ w = N = c ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ c ∧ 1 st ⁡ c = N
76 75 3 70 3eqtr4g ⊢ G ∈ USHGraph ∧ N ∈ ℕ → C = c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w | 1 st ⁡ c = N
77 clwwlkn ⊢ N ClWWalksN G = s ∈ ClWWalks ⁡ G | s = N
78 77 a1i ⊢ G ∈ USHGraph ∧ N ∈ ℕ → N ClWWalksN G = s ∈ ClWWalks ⁡ G | s = N
79 73 76 78 f1oeq123d ⊢ G ∈ USHGraph ∧ N ∈ ℕ → F : C ⟶ 1-1 onto N ClWWalksN G ↔ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ 2 nd ⁡ c prefix 2 nd ⁡ c − 1 ↾ c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w | 1 st ⁡ c = N : c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w | 1 st ⁡ c = N ⟶ 1-1 onto s ∈ ClWWalks ⁡ G | s = N
80 42 79 mpbird ⊢ G ∈ USHGraph ∧ N ∈ ℕ → F : C ⟶ 1-1 onto N ClWWalksN G