Metamath Proof Explorer

Theorem wlkiswwlksupgr2

Description: A walk as word corresponds to the sequence of vertices in a walk in a pseudograph. This variant of wlkiswwlks2 does not require G to be a simple pseudograph, but it requires the Axiom of Choice ( ac6 ) for its proof. Notice that only the existence of a function f can be proven, but, in general, it cannot be "constructed" (as in wlkiswwlks2 ). (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 10-Apr-2021)

Ref Expression
Assertion wlkiswwlksupgr2 ( 𝐺 ∈ UPGraph → ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 iswwlks ⊢ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
4 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
5 4 eleq2i ⊢ ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran ( iEdg ‘ 𝐺 ) )
6 upgruhgr ⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
7 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
8 7 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
9 6 8 syl ⊢ ( 𝐺 ∈ UPGraph → Fun ( iEdg ‘ 𝐺 ) )
10 9 adantl ⊢ ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) → Fun ( iEdg ‘ 𝐺 ) )
11 elrnrexdm ⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran ( iEdg ‘ 𝐺 ) → ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
12 eqcom ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
13 12 rexbii ⊢ ( ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
14 11 13 imbitrrdi ⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran ( iEdg ‘ 𝐺 ) → ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
15 10 14 syl ⊢ ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran ( iEdg ‘ 𝐺 ) → ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
16 5 15 biimtrid ⊢ ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
17 16 ralimdv ⊢ ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
18 17 ex ⊢ ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ∈ UPGraph → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
19 18 com23 ⊢ ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝐺 ∈ UPGraph → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
20 19 3impia ⊢ ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐺 ∈ UPGraph → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
21 20 impcom ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } )
22 ovex ⊢ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ V
23 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
24 23 dmex ⊢ dom ( iEdg ‘ 𝐺 ) ∈ V
25 fveqeq2 ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑖 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
26 22 24 25 ac6 ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ∃ 𝑓 ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
27 21 26 syl ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑓 ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
28 iswrdi ⊢ ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) )
29 28 adantr ⊢ ( ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) )
30 29 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) )
31 len0nnbi ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑃 ≠ ∅ ↔ ( ♯ ‘ 𝑃 ) ∈ ℕ ) )
32 31 biimpac ⊢ ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ )
33 wrdf ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
34 nnz ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( ♯ ‘ 𝑃 ) ∈ ℤ )
35 fzoval ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
36 34 35 syl ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
37 36 adantr ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
38 nnm1nn0 ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 )
39 fnfzo0hash ⊢ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
40 38 39 sylan ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
41 40 eqcomd ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝑓 ) )
42 41 oveq2d ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) → ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 0 ... ( ♯ ‘ 𝑓 ) ) )
43 37 42 eqtrd ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ♯ ‘ 𝑓 ) ) )
44 43 feq2d ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
45 44 biimpcd ⊢ ( 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
46 45 expd ⊢ ( 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) )
47 33 46 syl ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) )
48 47 adantl ⊢ ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) )
49 32 48 mpd ⊢ ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
50 49 3adant3 ⊢ ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
51 50 adantl ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
52 51 com12 ⊢ ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
53 52 adantr ⊢ ( ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
54 53 impcom ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
55 simpr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } )
56 32 40 sylan ⊢ ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
57 56 oveq2d ⊢ ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
58 57 ex ⊢ ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) )
59 58 3adant3 ⊢ ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) )
60 59 adantl ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) )
61 60 imp ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
62 61 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
63 55 62 raleqtrrdv ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } )
64 63 anasss ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } )
65 30 54 64 3jca ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
66 65 ex ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
67 66 eximdv ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ∃ 𝑓 ( 𝑓 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ∃ 𝑓 ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
68 27 67 mpd ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑓 ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
69 1 7 upgriswlk ⊢ ( 𝐺 ∈ UPGraph → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
70 69 adantr ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
71 70 exbidv ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ↔ ∃ 𝑓 ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
72 68 71 mpbird ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 )
73 72 ex ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )
74 3 73 biimtrid ⊢ ( 𝐺 ∈ UPGraph → ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )