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∈UPGraph→P∈WWalks⁡G→∃ffWalks⁡GP

Proof

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