This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
clwlkclwwlkf.f ⊢ 𝐹 = ( 𝑐 ∈ 𝐶 ↦ ( ( 2nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2nd ‘ 𝑐 ) ) − 1 ) ) )
Assertion clwlkclwwlkfo ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 –onto→ ( ClWWalks ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
2 clwlkclwwlkf.f ⊢ 𝐹 = ( 𝑐 ∈ 𝐶 ↦ ( ( 2nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2nd ‘ 𝑐 ) ) − 1 ) ) )
3 1 2 clwlkclwwlkf ⊢ ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 ⟶ ( ClWWalks ‘ 𝐺 ) )
4 clwwlkgt0 ⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → 0 < ( ♯ ‘ 𝑤 ) )
5 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
6 5 clwwlkbp ⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑤 ≠ ∅ ) )
7 lencl ⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑤 ) ∈ ℕ0 )
8 7 nn0zd ⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑤 ) ∈ ℤ )
9 zgt0ge1 ⊢ ( ( ♯ ‘ 𝑤 ) ∈ ℤ → ( 0 < ( ♯ ‘ 𝑤 ) ↔ 1 ≤ ( ♯ ‘ 𝑤 ) ) )
10 8 9 syl ⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( 0 < ( ♯ ‘ 𝑤 ) ↔ 1 ≤ ( ♯ ‘ 𝑤 ) ) )
11 10 biimpd ⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( 0 < ( ♯ ‘ 𝑤 ) → 1 ≤ ( ♯ ‘ 𝑤 ) ) )
12 11 anc2li ⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( 0 < ( ♯ ‘ 𝑤 ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) )
13 12 3ad2ant2 ⊢ ( ( 𝐺 ∈ V ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑤 ≠ ∅ ) → ( 0 < ( ♯ ‘ 𝑤 ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) )
14 6 13 syl ⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( 0 < ( ♯ ‘ 𝑤 ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) )
15 4 14 mpd ⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) )
16 15 adantl ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) )
17 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
18 5 17 clwlkclwwlk2 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ( ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ↔ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ) )
19 df-br ⊢ ( 𝑓 ( ClWalks ‘ 𝐺 ) ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ↔ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) )
20 simpr2 ⊢ ( ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
21 simpr3 ⊢ ( ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) → 1 ≤ ( ♯ ‘ 𝑤 ) )
22 simpl ⊢ ( ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) → ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) )
23 1 clwlkclwwlkfolem ⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ 𝐶 )
24 20 21 22 23 syl3anc ⊢ ( ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) → ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ 𝐶 )
25 23 3expa ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ 𝐶 )
26 ovex ⊢ ( ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) prefix ( ( ♯ ‘ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ) − 1 ) ) ∈ V
27 fveq2 ⊢ ( 𝑐 = ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ → ( 2nd ‘ 𝑐 ) = ( 2nd ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) )
28 2fveq3 ⊢ ( 𝑐 = ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ → ( ♯ ‘ ( 2nd ‘ 𝑐 ) ) = ( ♯ ‘ ( 2nd ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) )
29 28 oveq1d ⊢ ( 𝑐 = ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ → ( ( ♯ ‘ ( 2nd ‘ 𝑐 ) ) − 1 ) = ( ( ♯ ‘ ( 2nd ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) − 1 ) )
30 27 29 oveq12d ⊢ ( 𝑐 = ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ → ( ( 2nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2nd ‘ 𝑐 ) ) − 1 ) ) = ( ( 2nd ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) prefix ( ( ♯ ‘ ( 2nd ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) − 1 ) ) )
31 vex ⊢ 𝑓 ∈ V
32 ovex ⊢ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ∈ V
33 31 32 op2nd ⊢ ( 2nd ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) = ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ )
34 33 fveq2i ⊢ ( ♯ ‘ ( 2nd ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) = ( ♯ ‘ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) )
35 34 oveq1i ⊢ ( ( ♯ ‘ ( 2nd ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) − 1 ) = ( ( ♯ ‘ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ) − 1 )
36 33 35 oveq12i ⊢ ( ( 2nd ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) prefix ( ( ♯ ‘ ( 2nd ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) − 1 ) ) = ( ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) prefix ( ( ♯ ‘ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ) − 1 ) )
37 30 36 eqtrdi ⊢ ( 𝑐 = ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ → ( ( 2nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2nd ‘ 𝑐 ) ) − 1 ) ) = ( ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) prefix ( ( ♯ ‘ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ) − 1 ) ) )
38 37 2 fvmptg ⊢ ( ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ 𝐶 ∧ ( ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) prefix ( ( ♯ ‘ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ) − 1 ) ) ∈ V ) → ( 𝐹 ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) = ( ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) prefix ( ( ♯ ‘ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ) − 1 ) ) )
39 25 26 38 sylancl ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ( 𝐹 ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) = ( ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) prefix ( ( ♯ ‘ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ) − 1 ) ) )
40 wrdlenccats1lenm1 ⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ) − 1 ) = ( ♯ ‘ 𝑤 ) )
41 40 ad2antrr ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ) − 1 ) = ( ♯ ‘ 𝑤 ) )
42 41 oveq2d ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ( ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) prefix ( ( ♯ ‘ ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ) − 1 ) ) = ( ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) prefix ( ♯ ‘ 𝑤 ) ) )
43 simpll ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
44 simpl ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) )
45 wrdsymb1 ⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
46 44 45 syl ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
47 46 s1cld ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
48 eqidd ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑤 ) )
49 pfxccatid ⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑤 ) ) → ( ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) prefix ( ♯ ‘ 𝑤 ) ) = 𝑤 )
50 43 47 48 49 syl3anc ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ( ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) prefix ( ♯ ‘ 𝑤 ) ) = 𝑤 )
51 39 42 50 3eqtrrd ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ∧ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → 𝑤 = ( 𝐹 ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) )
52 51 ex ⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → 𝑤 = ( 𝐹 ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) )
53 52 3adant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → 𝑤 = ( 𝐹 ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) )
54 53 ad2antlr ⊢ ( ( ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) ∧ 𝑐 = ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) → ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → 𝑤 = ( 𝐹 ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) )
55 fveq2 ⊢ ( 𝑐 = ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) )
56 55 eqeq2d ⊢ ( 𝑐 = ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ → ( 𝑤 = ( 𝐹 ‘ 𝑐 ) ↔ 𝑤 = ( 𝐹 ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) )
57 56 imbi2d ⊢ ( 𝑐 = ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ → ( ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → 𝑤 = ( 𝐹 ‘ 𝑐 ) ) ↔ ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → 𝑤 = ( 𝐹 ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) ) )
58 57 adantl ⊢ ( ( ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) ∧ 𝑐 = ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) → ( ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → 𝑤 = ( 𝐹 ‘ 𝑐 ) ) ↔ ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → 𝑤 = ( 𝐹 ‘ ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) ) ) )
59 54 58 mpbird ⊢ ( ( ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) ∧ 𝑐 = ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ) → ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → 𝑤 = ( 𝐹 ‘ 𝑐 ) ) )
60 24 59 rspcimedv ⊢ ( ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) → ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) ) )
61 60 ex ⊢ ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) ) ) )
62 61 pm2.43b ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ( ⟨ 𝑓 , ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) ) )
63 19 62 biimtrid ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ( 𝑓 ( ClWalks ‘ 𝐺 ) ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) → ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) ) )
64 63 exlimdv ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ( ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) ( 𝑤 ++ ⟨“ ( 𝑤 ‘ 0 ) ”⟩ ) → ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) ) )
65 18 64 sylbird ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) ) )
66 65 3expib ⊢ ( 𝐺 ∈ USPGraph → ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) ) ) )
67 66 com23 ⊢ ( 𝐺 ∈ USPGraph → ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) ) ) )
68 67 imp ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ) → ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑤 ) ) → ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) ) )
69 16 68 mpd ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ) → ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) )
70 69 ralrimiva ⊢ ( 𝐺 ∈ USPGraph → ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) )
71 dffo3 ⊢ ( 𝐹 : 𝐶 –onto→ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝐹 : 𝐶 ⟶ ( ClWWalks ‘ 𝐺 ) ∧ ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∃ 𝑐 ∈ 𝐶 𝑤 = ( 𝐹 ‘ 𝑐 ) ) )
72 3 70 71 sylanbrc ⊢ ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 –onto→ ( ClWWalks ‘ 𝐺 ) )