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 ${⊢}{G}\in \mathrm{UPGraph}\to \left({P}\in \mathrm{WWalks}\left({G}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{Walks}\left({G}\right){P}\right)$

Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
2 eqid ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{Edg}\left({G}\right)$
3 1 2 iswwlks ${⊢}{P}\in \mathrm{WWalks}\left({G}\right)↔\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
4 edgval ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{ran}\mathrm{iEdg}\left({G}\right)$
5 4 eleq2i ${⊢}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)↔\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}\mathrm{iEdg}\left({G}\right)$
6 upgruhgr ${⊢}{G}\in \mathrm{UPGraph}\to {G}\in \mathrm{UHGraph}$
7 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({G}\right)$
8 7 uhgrfun ${⊢}{G}\in \mathrm{UHGraph}\to \mathrm{Fun}\mathrm{iEdg}\left({G}\right)$
9 6 8 syl ${⊢}{G}\in \mathrm{UPGraph}\to \mathrm{Fun}\mathrm{iEdg}\left({G}\right)$
10 9 adantl ${⊢}\left(\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\wedge {G}\in \mathrm{UPGraph}\right)\to \mathrm{Fun}\mathrm{iEdg}\left({G}\right)$
11 elrnrexdm ${⊢}\mathrm{Fun}\mathrm{iEdg}\left({G}\right)\to \left(\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}\mathrm{iEdg}\left({G}\right)\to \exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}=\mathrm{iEdg}\left({G}\right)\left({x}\right)\right)$
12 eqcom ${⊢}\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}↔\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}=\mathrm{iEdg}\left({G}\right)\left({x}\right)$
13 12 rexbii ${⊢}\exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}↔\exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}=\mathrm{iEdg}\left({G}\right)\left({x}\right)$
14 11 13 syl6ibr ${⊢}\mathrm{Fun}\mathrm{iEdg}\left({G}\right)\to \left(\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}\mathrm{iEdg}\left({G}\right)\to \exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
15 10 14 syl ${⊢}\left(\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\wedge {G}\in \mathrm{UPGraph}\right)\to \left(\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}\mathrm{iEdg}\left({G}\right)\to \exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
16 5 15 syl5bi ${⊢}\left(\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\wedge {G}\in \mathrm{UPGraph}\right)\to \left(\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\to \exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
17 16 ralimdv ${⊢}\left(\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\wedge {G}\in \mathrm{UPGraph}\right)\to \left(\forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\to \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
18 17 ex ${⊢}\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left({G}\in \mathrm{UPGraph}\to \left(\forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\to \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\right)$
19 18 com23 ${⊢}\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\to \left({G}\in \mathrm{UPGraph}\to \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\right)$
20 19 3impia ${⊢}\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to \left({G}\in \mathrm{UPGraph}\to \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
21 20 impcom ${⊢}\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}$
22 ovex ${⊢}\left(0..^\left|{P}\right|-1\right)\in \mathrm{V}$
23 fvex ${⊢}\mathrm{iEdg}\left({G}\right)\in \mathrm{V}$
24 23 dmex ${⊢}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\in \mathrm{V}$
25 fveqeq2 ${⊢}{x}={f}\left({i}\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}↔\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
26 22 24 25 ac6 ${⊢}\forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\exists {x}\in \mathrm{dom}\mathrm{iEdg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({x}\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
27 21 26 syl ${⊢}\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
28 iswrdi ${⊢}{f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to {f}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)$
29 28 adantr ${⊢}\left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\to {f}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)$
30 29 adantl ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\right)\to {f}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)$
31 len0nnbi ${⊢}{P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to \left({P}\ne \varnothing ↔\left|{P}\right|\in ℕ\right)$
32 31 biimpac ${⊢}\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left|{P}\right|\in ℕ$
33 wrdf ${⊢}{P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to {P}:\left(0..^\left|{P}\right|\right)⟶\mathrm{Vtx}\left({G}\right)$
34 nnz ${⊢}\left|{P}\right|\in ℕ\to \left|{P}\right|\in ℤ$
35 fzoval ${⊢}\left|{P}\right|\in ℤ\to \left(0..^\left|{P}\right|\right)=\left(0\dots \left|{P}\right|-1\right)$
36 34 35 syl ${⊢}\left|{P}\right|\in ℕ\to \left(0..^\left|{P}\right|\right)=\left(0\dots \left|{P}\right|-1\right)$
37 36 adantr ${⊢}\left(\left|{P}\right|\in ℕ\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(0..^\left|{P}\right|\right)=\left(0\dots \left|{P}\right|-1\right)$
38 nnm1nn0 ${⊢}\left|{P}\right|\in ℕ\to \left|{P}\right|-1\in {ℕ}_{0}$
39 fnfzo0hash ${⊢}\left(\left|{P}\right|-1\in {ℕ}_{0}\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left|{f}\right|=\left|{P}\right|-1$
40 38 39 sylan ${⊢}\left(\left|{P}\right|\in ℕ\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left|{f}\right|=\left|{P}\right|-1$
41 40 eqcomd ${⊢}\left(\left|{P}\right|\in ℕ\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left|{P}\right|-1=\left|{f}\right|$
42 41 oveq2d ${⊢}\left(\left|{P}\right|\in ℕ\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(0\dots \left|{P}\right|-1\right)=\left(0\dots \left|{f}\right|\right)$
43 37 42 eqtrd ${⊢}\left(\left|{P}\right|\in ℕ\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(0..^\left|{P}\right|\right)=\left(0\dots \left|{f}\right|\right)$
44 43 feq2d ${⊢}\left(\left|{P}\right|\in ℕ\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left({P}:\left(0..^\left|{P}\right|\right)⟶\mathrm{Vtx}\left({G}\right)↔{P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\right)$
45 44 biimpcd ${⊢}{P}:\left(0..^\left|{P}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\to \left(\left(\left|{P}\right|\in ℕ\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\right)$
46 45 expd ${⊢}{P}:\left(0..^\left|{P}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\to \left(\left|{P}\right|\in ℕ\to \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\right)\right)$
47 33 46 syl ${⊢}{P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to \left(\left|{P}\right|\in ℕ\to \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\right)\right)$
48 47 adantl ${⊢}\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left(\left|{P}\right|\in ℕ\to \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\right)\right)$
49 32 48 mpd ${⊢}\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\right)$
50 49 3adant3 ${⊢}\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\right)$
51 50 adantl ${⊢}\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\right)$
52 51 com12 ${⊢}{f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to \left(\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\right)$
53 52 adantr ${⊢}\left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\to \left(\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\right)$
54 53 impcom ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\right)\to {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)$
55 simpr ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\to \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}$
56 32 40 sylan ${⊢}\left(\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left|{f}\right|=\left|{P}\right|-1$
57 56 oveq2d ${⊢}\left(\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(0..^\left|{f}\right|\right)=\left(0..^\left|{P}\right|-1\right)$
58 57 ex ${⊢}\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to \left(0..^\left|{f}\right|\right)=\left(0..^\left|{P}\right|-1\right)\right)$
59 58 3adant3 ${⊢}\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to \left(0..^\left|{f}\right|\right)=\left(0..^\left|{P}\right|-1\right)\right)$
60 59 adantl ${⊢}\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to \left(0..^\left|{f}\right|\right)=\left(0..^\left|{P}\right|-1\right)\right)$
61 60 imp ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(0..^\left|{f}\right|\right)=\left(0..^\left|{P}\right|-1\right)$
62 61 adantr ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\to \left(0..^\left|{f}\right|\right)=\left(0..^\left|{P}\right|-1\right)$
63 62 raleqdv ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\to \left(\forall {i}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}↔\forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
64 55 63 mpbird ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge {f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\to \forall {i}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}$
65 64 anasss ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\right)\to \forall {i}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}$
66 30 54 65 3jca ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\right)\to \left({f}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
67 66 ex ${⊢}\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \left(\left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\to \left({f}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\right)$
68 67 eximdv ${⊢}\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\left(0..^\left|{P}\right|-1\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\right)$
69 27 68 mpd ${⊢}\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
70 1 7 upgriswlk ${⊢}{G}\in \mathrm{UPGraph}\to \left({f}\mathrm{Walks}\left({G}\right){P}↔\left({f}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\right)$
71 70 adantr ${⊢}\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \left({f}\mathrm{Walks}\left({G}\right){P}↔\left({f}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\right)$
72 71 exbidv ${⊢}\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{Walks}\left({G}\right){P}↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge {P}:\left(0\dots \left|{f}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({f}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)\right)$
73 69 72 mpbird ${⊢}\left({G}\in \mathrm{UPGraph}\wedge \left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{Walks}\left({G}\right){P}$
74 73 ex ${⊢}{G}\in \mathrm{UPGraph}\to \left(\left({P}\ne \varnothing \wedge {P}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{P}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{Walks}\left({G}\right){P}\right)$
75 3 74 syl5bi ${⊢}{G}\in \mathrm{UPGraph}\to \left({P}\in \mathrm{WWalks}\left({G}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{Walks}\left({G}\right){P}\right)$