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 → ∃ f f Walks ⁡ G P

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 ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G
4 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
5 4 eleq2i ⊢ P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ↔ P ⁡ i P ⁡ 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 ∈ Word Vtx ⁡ G ∧ G ∈ UPGraph → Fun ⁡ iEdg ⁡ G
11 elrnrexdm ⊢ Fun ⁡ iEdg ⁡ G → P ⁡ i P ⁡ i + 1 ∈ ran ⁡ iEdg ⁡ G → ∃ x ∈ dom ⁡ iEdg ⁡ G P ⁡ i P ⁡ i + 1 = iEdg ⁡ G ⁡ x
12 eqcom ⊢ iEdg ⁡ G ⁡ x = P ⁡ i P ⁡ i + 1 ↔ P ⁡ i P ⁡ i + 1 = iEdg ⁡ G ⁡ x
13 12 rexbii ⊢ ∃ x ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ G ⁡ x = P ⁡ i P ⁡ i + 1 ↔ ∃ x ∈ dom ⁡ iEdg ⁡ G P ⁡ i P ⁡ i + 1 = iEdg ⁡ G ⁡ x
14 11 13 imbitrrdi ⊢ Fun ⁡ iEdg ⁡ G → P ⁡ i P ⁡ i + 1 ∈ ran ⁡ iEdg ⁡ G → ∃ x ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ G ⁡ x = P ⁡ i P ⁡ i + 1
15 10 14 syl ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ G ∈ UPGraph → P ⁡ i P ⁡ i + 1 ∈ ran ⁡ iEdg ⁡ G → ∃ x ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ G ⁡ x = P ⁡ i P ⁡ i + 1
16 5 15 biimtrid ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ G ∈ UPGraph → P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → ∃ x ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ G ⁡ x = P ⁡ i P ⁡ i + 1
17 16 ralimdv ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ G ∈ UPGraph → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → ∀ i ∈ 0 ..^ P − 1 ∃ x ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ G ⁡ x = P ⁡ i P ⁡ i + 1
18 17 ex ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G → G ∈ UPGraph → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → ∀ i ∈ 0 ..^ P − 1 ∃ x ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ G ⁡ x = P ⁡ i P ⁡ i + 1
19 18 com23 ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → G ∈ UPGraph → ∀ i ∈ 0 ..^ P − 1 ∃ x ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ G ⁡ x = P ⁡ i P ⁡ i + 1
20 19 3impia ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → G ∈ UPGraph → ∀ i ∈ 0 ..^ P − 1 ∃ x ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ G ⁡ x = P ⁡ i P ⁡ i + 1
21 20 impcom ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → ∀ i ∈ 0 ..^ P − 1 ∃ x ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ G ⁡ x = P ⁡ i P ⁡ 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 ⁡ i P ⁡ i + 1 ↔ iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
26 22 24 25 ac6 ⊢ ∀ i ∈ 0 ..^ P − 1 ∃ x ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ G ⁡ x = P ⁡ i P ⁡ i + 1 → ∃ f f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
27 21 26 syl ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → ∃ f f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
28 iswrdi ⊢ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G → f ∈ Word dom ⁡ iEdg ⁡ G
29 28 adantr ⊢ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → f ∈ Word dom ⁡ iEdg ⁡ G
30 29 adantl ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → f ∈ Word dom ⁡ iEdg ⁡ G
31 len0nnbi ⊢ P ∈ Word Vtx ⁡ G → P ≠ ∅ ↔ P ∈ ℕ
32 31 biimpac ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G → P ∈ ℕ
33 wrdf ⊢ P ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ G → P ∈ ℕ → f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G → P : 0 … f ⟶ Vtx ⁡ G
48 47 adantl ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G → P ∈ ℕ → f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G → P : 0 … f ⟶ Vtx ⁡ G
49 32 48 mpd ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G → f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G → P : 0 … f ⟶ Vtx ⁡ G
50 49 3adant3 ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G → P : 0 … f ⟶ Vtx ⁡ G
51 50 adantl ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ 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 ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → P : 0 … f ⟶ Vtx ⁡ G
53 52 adantr ⊢ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → P : 0 … f ⟶ Vtx ⁡ G
54 53 impcom ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → P : 0 … f ⟶ Vtx ⁡ G
55 simpr ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
56 32 40 sylan ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G → f = P − 1
57 56 oveq2d ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G → 0 ..^ f = 0 ..^ P − 1
58 57 ex ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G → f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G → 0 ..^ f = 0 ..^ P − 1
59 58 3adant3 ⊢ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G → 0 ..^ f = 0 ..^ P − 1
60 59 adantl ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G → 0 ..^ f = 0 ..^ P − 1
61 60 imp ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G → 0 ..^ f = 0 ..^ P − 1
62 61 adantr ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → 0 ..^ f = 0 ..^ P − 1
63 55 62 raleqtrrdv ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → ∀ i ∈ 0 ..^ f iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
64 63 anasss ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → ∀ i ∈ 0 ..^ f iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
65 30 54 64 3jca ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → f ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … f ⟶ Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ f iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
66 65 ex ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → f ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … f ⟶ Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ f iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
67 66 eximdv ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → ∃ f f : 0 ..^ P − 1 ⟶ dom ⁡ iEdg ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → ∃ f f ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … f ⟶ Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ f iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
68 27 67 mpd ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → ∃ f f ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … f ⟶ Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ f iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
69 1 7 upgriswlk ⊢ G ∈ UPGraph → f Walks ⁡ G P ↔ f ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … f ⟶ Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ f iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
70 69 adantr ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → f Walks ⁡ G P ↔ f ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … f ⟶ Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ f iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
71 70 exbidv ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → ∃ f f Walks ⁡ G P ↔ ∃ f f ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … f ⟶ Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ f iEdg ⁡ G ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
72 68 71 mpbird ⊢ G ∈ UPGraph ∧ P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → ∃ f f Walks ⁡ G P
73 72 ex ⊢ G ∈ UPGraph → P ≠ ∅ ∧ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G → ∃ f f Walks ⁡ G P
74 3 73 biimtrid ⊢ G ∈ UPGraph → P ∈ WWalks ⁡ G → ∃ f f Walks ⁡ G P