Step | Hyp | Ref
| Expression |
1 | | wwlkprop 26213 |
. . 3
⊢ (𝑃 ∈ (𝑉 WWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉)) |
2 | | iswwlk 26211 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ (𝑉 WWalks 𝐸) ↔ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))) |
3 | 2 | 3adant3 1074 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) → (𝑃 ∈ (𝑉 WWalks 𝐸) ↔ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))) |
4 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢
(0..^((#‘𝑃)
− 1)) ∈ V |
5 | | mptexg 6389 |
. . . . . . . . . . . . . . 15
⊢
((0..^((#‘𝑃)
− 1)) ∈ V → (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ∈ V) |
6 | 4, 5 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸)) → (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ∈ V) |
7 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸) → 𝑉 USGrph 𝐸) |
8 | 7 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸)) → 𝑉 USGrph 𝐸) |
9 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) → 𝑃 ∈ Word 𝑉) |
10 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸)) → 𝑃 ∈ Word 𝑉) |
11 | | hashge1 13039 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅) → 1 ≤ (#‘𝑃)) |
12 | 11 | ancoms 468 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) → 1 ≤ (#‘𝑃)) |
13 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸)) → 1 ≤ (#‘𝑃)) |
14 | 8, 10, 13 | 3jca 1235 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸)) → (𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃))) |
15 | 14 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸)) ∧ 𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))) → (𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃))) |
16 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
17 | 16 | wlkiswwlk2lem6 26224 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))(𝐸‘((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸)) ∧ 𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))(𝐸‘((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
19 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) → (𝑓 ∈ Word dom 𝐸 ↔ (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ∈ Word dom 𝐸)) |
20 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) → (#‘𝑓) = (#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})))) |
21 | 20 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) → (0...(#‘𝑓)) = (0...(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))) |
22 | 21 | feq2d 5944 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) → (𝑃:(0...(#‘𝑓))⟶𝑉 ↔ 𝑃:(0...(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))⟶𝑉)) |
23 | 20 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) → (0..^(#‘𝑓)) = (0..^(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))) |
24 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) → (𝑓‘𝑖) = ((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))‘𝑖)) |
25 | 24 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) → (𝐸‘(𝑓‘𝑖)) = (𝐸‘((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))‘𝑖))) |
26 | 25 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) → ((𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (𝐸‘((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
27 | 23, 26 | raleqbidv 3129 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) → (∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ (0..^(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))(𝐸‘((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
28 | 19, 22, 27 | 3anbi123d 1391 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) → ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ↔ ((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))(𝐸‘((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
29 | 28 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) → ((∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))(𝐸‘((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))) |
30 | 29 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸)) ∧ 𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))) → ((∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘(𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))))(𝐸‘((𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))) |
31 | 18, 30 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸)) ∧ 𝑓 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
32 | 6, 31 | spcimedv 3265 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∃𝑓(𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
33 | 32 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) → (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∃𝑓(𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))) |
34 | 33 | com23 84 |
. . . . . . . . . . 11
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸) → ∃𝑓(𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))) |
35 | 34 | 3impia 1253 |
. . . . . . . . . 10
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑉 USGrph 𝐸) → ∃𝑓(𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
36 | 35 | expd 451 |
. . . . . . . . 9
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) → (𝑉 USGrph 𝐸 → ∃𝑓(𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))) |
37 | 36 | impcom 445 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) → (𝑉 USGrph 𝐸 → ∃𝑓(𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
38 | 37 | imp 444 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) ∧ 𝑉 USGrph 𝐸) → ∃𝑓(𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
39 | | 3simpa 1051 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
40 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
41 | 40 | jctl 562 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ Word 𝑉 → (𝑓 ∈ V ∧ 𝑃 ∈ Word 𝑉)) |
42 | 41 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) → (𝑓 ∈ V ∧ 𝑃 ∈ Word 𝑉)) |
43 | 39, 42 | jca 553 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑓 ∈ V ∧ 𝑃 ∈ Word 𝑉))) |
44 | 43 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑓 ∈ V ∧ 𝑃 ∈ Word 𝑉))) |
45 | 44 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) ∧ 𝑉 USGrph 𝐸) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑓 ∈ V ∧ 𝑃 ∈ Word 𝑉))) |
46 | | iswlk 26048 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑓 ∈ V ∧ 𝑃 ∈ Word 𝑉)) → (𝑓(𝑉 Walks 𝐸)𝑃 ↔ (𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
47 | 45, 46 | syl 17 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) ∧ 𝑉 USGrph 𝐸) → (𝑓(𝑉 Walks 𝐸)𝑃 ↔ (𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
48 | 47 | exbidv 1837 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) ∧ 𝑉 USGrph 𝐸) → (∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃 ↔ ∃𝑓(𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
49 | 38, 48 | mpbird 246 |
. . . . . 6
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) ∧ 𝑉 USGrph 𝐸) → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃) |
50 | 49 | ex 449 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) → (𝑉 USGrph 𝐸 → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃)) |
51 | 50 | ex 449 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) → ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑉 USGrph 𝐸 → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃))) |
52 | 3, 51 | sylbid 229 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) → (𝑃 ∈ (𝑉 WWalks 𝐸) → (𝑉 USGrph 𝐸 → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃))) |
53 | 1, 52 | mpcom 37 |
. 2
⊢ (𝑃 ∈ (𝑉 WWalks 𝐸) → (𝑉 USGrph 𝐸 → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃)) |
54 | 53 | com12 32 |
1
⊢ (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 WWalks 𝐸) → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃)) |