# 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}=\left\{{w}\in \mathrm{ClWalks}\left({G}\right)|1\le \left|{1}^{st}\left({w}\right)\right|\right\}$
clwlkclwwlkf.f ${⊢}{F}=\left({c}\in {C}⟼{2}^{nd}\left({c}\right)\mathrm{prefix}\left(\left|{2}^{nd}\left({c}\right)\right|-1\right)\right)$
Assertion clwlkclwwlkfo ${⊢}{G}\in \mathrm{USHGraph}\to {F}:{C}\underset{onto}{⟶}\mathrm{ClWWalks}\left({G}\right)$

### Proof

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