# 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}\left({c}\right)$
clwlknf1oclwwlkn.b ${⊢}{B}={2}^{nd}\left({c}\right)$
clwlknf1oclwwlkn.c ${⊢}{C}=\left\{{w}\in \mathrm{ClWalks}\left({G}\right)|\left|{1}^{st}\left({w}\right)\right|={N}\right\}$
clwlknf1oclwwlkn.f ${⊢}{F}=\left({c}\in {C}⟼{B}\mathrm{prefix}\left|{A}\right|\right)$
Assertion clwlknf1oclwwlkn ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {N}\in ℕ\right)\to {F}:{C}\underset{1-1 onto}{⟶}{N}\mathrm{ClWWalksN}{G}$

### Proof

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