Proof of Theorem iswlkg
Step | Hyp | Ref
| Expression |
1 | | wlkbprop 26051 |
. . 3
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
2 | | iswlk 26048 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
3 | 2 | biimpd 218 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
4 | 3 | 3adant1 1072 |
. . 3
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
5 | 1, 4 | mpcom 37 |
. 2
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
6 | | ovex 6577 |
. . . . . . . . . . 11
⊢
(0...(#‘𝐹))
∈ V |
7 | | fpmg 7769 |
. . . . . . . . . . 11
⊢
(((0...(#‘𝐹))
∈ V ∧ 𝑉 ∈
𝑋 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹)))) |
8 | 6, 7 | mp3an1 1403 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹)))) |
9 | 8 | ex 449 |
. . . . . . . . 9
⊢ (𝑉 ∈ 𝑋 → (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹))))) |
10 | 9 | anim2d 587 |
. . . . . . . 8
⊢ (𝑉 ∈ 𝑋 → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹)))))) |
11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹)))))) |
12 | 11 | com12 32 |
. . . . . 6
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹)))))) |
13 | 12 | 3adant3 1074 |
. . . . 5
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹)))))) |
14 | 13 | impcom 445 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹))))) |
15 | | iswlk 26048 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹))))) →
(𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
16 | 15 | biimprd 237 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹))))) →
((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → 𝐹(𝑉 Walks 𝐸)𝑃)) |
17 | 16 | expcom 450 |
. . . . 5
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹)))) →
((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → 𝐹(𝑉 Walks 𝐸)𝑃))) |
18 | 17 | impd 446 |
. . . 4
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃 ∈ (𝑉 ↑pm
(0...(#‘𝐹)))) →
(((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → 𝐹(𝑉 Walks 𝐸)𝑃)) |
19 | 14, 18 | mpcom 37 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → 𝐹(𝑉 Walks 𝐸)𝑃) |
20 | 19 | ex 449 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → 𝐹(𝑉 Walks 𝐸)𝑃)) |
21 | 5, 20 | impbid2 215 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |