Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | eqid 2622 |
. . 3
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
3 | 1, 2 | iswwlks 26728 |
. 2
⊢ (𝑃 ∈ (WWalks‘𝐺) ↔ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
4 | | edgval 25941 |
. . . . . . . . . . . . 13
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
5 | 4 | eleq2i 2693 |
. . . . . . . . . . . 12
⊢ ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺)) |
6 | | upgruhgr 25997 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph
) |
7 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
8 | 7 | uhgrfun 25961 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
9 | 6, 8 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ UPGraph → Fun
(iEdg‘𝐺)) |
10 | 9 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) → Fun
(iEdg‘𝐺)) |
11 | | elrnrexdm 6363 |
. . . . . . . . . . . . . 14
⊢ (Fun
(iEdg‘𝐺) →
({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) → ∃𝑥 ∈ dom (iEdg‘𝐺){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = ((iEdg‘𝐺)‘𝑥))) |
12 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = ((iEdg‘𝐺)‘𝑥)) |
13 | 12 | rexbii 3041 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∃𝑥 ∈ dom (iEdg‘𝐺){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = ((iEdg‘𝐺)‘𝑥)) |
14 | 11, 13 | syl6ibr 242 |
. . . . . . . . . . . . 13
⊢ (Fun
(iEdg‘𝐺) →
({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) → ∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
15 | 10, 14 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) → ∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
16 | 5, 15 | syl5bi 232 |
. . . . . . . . . . 11
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
17 | 16 | ralimdv 2963 |
. . . . . . . . . 10
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
18 | 17 | ex 450 |
. . . . . . . . 9
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → (𝐺 ∈ UPGraph → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
19 | 18 | com23 86 |
. . . . . . . 8
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝐺 ∈ UPGraph → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
20 | 19 | 3impia 1261 |
. . . . . . 7
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝐺 ∈ UPGraph → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
21 | 20 | impcom 446 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
22 | | ovex 6678 |
. . . . . . 7
⊢
(0..^((#‘𝑃)
− 1)) ∈ V |
23 | | fvex 6201 |
. . . . . . . 8
⊢
(iEdg‘𝐺)
∈ V |
24 | 23 | dmex 7099 |
. . . . . . 7
⊢ dom
(iEdg‘𝐺) ∈
V |
25 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = (𝑓‘𝑖) → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘(𝑓‘𝑖))) |
26 | 25 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑥 = (𝑓‘𝑖) → (((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
27 | 22, 24, 26 | ac6 9302 |
. . . . . 6
⊢
(∀𝑖 ∈
(0..^((#‘𝑃) −
1))∃𝑥 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∃𝑓(𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
28 | 21, 27 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → ∃𝑓(𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
29 | | iswrdi 13309 |
. . . . . . . . . 10
⊢ (𝑓:(0..^((#‘𝑃) − 1))⟶dom
(iEdg‘𝐺) → 𝑓 ∈ Word dom
(iEdg‘𝐺)) |
30 | 29 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑓:(0..^((#‘𝑃) − 1))⟶dom
(iEdg‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑃) −
1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → 𝑓 ∈ Word dom (iEdg‘𝐺)) |
31 | 30 | adantl 482 |
. . . . . . . 8
⊢ (((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → 𝑓 ∈ Word dom (iEdg‘𝐺)) |
32 | | wrdfin 13323 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → 𝑃 ∈ Fin) |
33 | | hashnncl 13157 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Fin →
((#‘𝑃) ∈ ℕ
↔ 𝑃 ≠
∅)) |
34 | 33 | bicomd 213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Fin → (𝑃 ≠ ∅ ↔
(#‘𝑃) ∈
ℕ)) |
35 | 32, 34 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → (𝑃 ≠ ∅ ↔ (#‘𝑃) ∈
ℕ)) |
36 | 35 | biimpac 503 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → (#‘𝑃) ∈
ℕ) |
37 | | wrdf 13310 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → 𝑃:(0..^(#‘𝑃))⟶(Vtx‘𝐺)) |
38 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑃) ∈
ℕ → (#‘𝑃)
∈ ℤ) |
39 | | fzoval 12471 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑃) ∈
ℤ → (0..^(#‘𝑃)) = (0...((#‘𝑃) − 1))) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑃) ∈
ℕ → (0..^(#‘𝑃)) = (0...((#‘𝑃) − 1))) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑃) ∈
ℕ ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (0..^(#‘𝑃)) = (0...((#‘𝑃) − 1))) |
42 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) ∈
ℕ → ((#‘𝑃)
− 1) ∈ ℕ0) |
43 | | fnfzo0hash 13234 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((#‘𝑃)
− 1) ∈ ℕ0 ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (#‘𝑓) = ((#‘𝑃) − 1)) |
44 | 42, 43 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑃) ∈
ℕ ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (#‘𝑓) = ((#‘𝑃) − 1)) |
45 | 44 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑃) ∈
ℕ ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → ((#‘𝑃) − 1) = (#‘𝑓)) |
46 | 45 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑃) ∈
ℕ ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (0...((#‘𝑃) − 1)) =
(0...(#‘𝑓))) |
47 | 41, 46 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑃) ∈
ℕ ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (0..^(#‘𝑃)) = (0...(#‘𝑓))) |
48 | 47 | feq2d 6031 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑃) ∈
ℕ ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (𝑃:(0..^(#‘𝑃))⟶(Vtx‘𝐺) ↔ 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺))) |
49 | 48 | biimpcd 239 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃:(0..^(#‘𝑃))⟶(Vtx‘𝐺) → (((#‘𝑃) ∈ ℕ ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺))) |
50 | 49 | expd 452 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃:(0..^(#‘𝑃))⟶(Vtx‘𝐺) → ((#‘𝑃) ∈ ℕ → (𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) → 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺)))) |
51 | 37, 50 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → ((#‘𝑃) ∈ ℕ → (𝑓:(0..^((#‘𝑃) − 1))⟶dom
(iEdg‘𝐺) → 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺)))) |
52 | 51 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → ((#‘𝑃) ∈ ℕ → (𝑓:(0..^((#‘𝑃) − 1))⟶dom
(iEdg‘𝐺) → 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺)))) |
53 | 36, 52 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → (𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) → 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺))) |
54 | 53 | 3adant3 1081 |
. . . . . . . . . . . 12
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) → 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺))) |
55 | 54 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) → 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺))) |
56 | 55 | com12 32 |
. . . . . . . . . 10
⊢ (𝑓:(0..^((#‘𝑃) − 1))⟶dom
(iEdg‘𝐺) →
((𝐺 ∈ UPGraph ∧
(𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺))) |
57 | 56 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑓:(0..^((#‘𝑃) − 1))⟶dom
(iEdg‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑃) −
1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺))) |
58 | 57 | impcom 446 |
. . . . . . . 8
⊢ (((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺)) |
59 | | simpr 477 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
60 | 36, 44 | sylan 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (#‘𝑓) = ((#‘𝑃) − 1)) |
61 | 60 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (0..^(#‘𝑓)) = (0..^((#‘𝑃) − 1))) |
62 | 61 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → (𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) → (0..^(#‘𝑓)) = (0..^((#‘𝑃) − 1)))) |
63 | 62 | 3adant3 1081 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) → (0..^(#‘𝑓)) = (0..^((#‘𝑃) − 1)))) |
64 | 63 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) → (0..^(#‘𝑓)) = (0..^((#‘𝑃) − 1)))) |
65 | 64 | imp 445 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (0..^(#‘𝑓)) = (0..^((#‘𝑃) − 1))) |
66 | 65 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (0..^(#‘𝑓)) = (0..^((#‘𝑃) − 1))) |
67 | 66 | raleqdv 3144 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (∀𝑖 ∈ (0..^(#‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
68 | 59, 67 | mpbird 247 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ 𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ∀𝑖 ∈ (0..^(#‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
69 | 68 | anasss 679 |
. . . . . . . 8
⊢ (((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ∀𝑖 ∈ (0..^(#‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
70 | 31, 58, 69 | 3jca 1242 |
. . . . . . 7
⊢ (((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
71 | 70 | ex 450 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → ((𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
72 | 71 | eximdv 1846 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (∃𝑓(𝑓:(0..^((#‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ∃𝑓(𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
73 | 28, 72 | mpd 15 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → ∃𝑓(𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
74 | 1, 7 | upgriswlk 26537 |
. . . . . 6
⊢ (𝐺 ∈ UPGraph → (𝑓(Walks‘𝐺)𝑃 ↔ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
75 | 74 | adantr 481 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (𝑓(Walks‘𝐺)𝑃 ↔ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
76 | 75 | exbidv 1850 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (∃𝑓 𝑓(Walks‘𝐺)𝑃 ↔ ∃𝑓(𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
77 | 73, 76 | mpbird 247 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → ∃𝑓 𝑓(Walks‘𝐺)𝑃) |
78 | 77 | ex 450 |
. 2
⊢ (𝐺 ∈ UPGraph → ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ∃𝑓 𝑓(Walks‘𝐺)𝑃)) |
79 | 3, 78 | syl5bi 232 |
1
⊢ (𝐺 ∈ UPGraph → (𝑃 ∈ (WWalks‘𝐺) → ∃𝑓 𝑓(Walks‘𝐺)𝑃)) |