Step | Hyp | Ref
| Expression |
1 | | iswlk 26048 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
2 | 1 | anbi1d 737 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2) ↔ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (#‘𝐹) = 2))) |
3 | | wrdf 13165 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
4 | | oveq2 6557 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
(0..^2)) |
5 | 4 | feq2d 5944 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ↔ 𝐹:(0..^2)⟶dom 𝐸)) |
6 | 3, 5 | syl5ib 233 |
. . . . . . . . 9
⊢
((#‘𝐹) = 2
→ (𝐹 ∈ Word dom
𝐸 → 𝐹:(0..^2)⟶dom 𝐸)) |
7 | | iswrdi 13164 |
. . . . . . . . 9
⊢ (𝐹:(0..^2)⟶dom 𝐸 → 𝐹 ∈ Word dom 𝐸) |
8 | 6, 7 | impbid1 214 |
. . . . . . . 8
⊢
((#‘𝐹) = 2
→ (𝐹 ∈ Word dom
𝐸 ↔ 𝐹:(0..^2)⟶dom 𝐸)) |
9 | 8 | adantl 481 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) ∧ (#‘𝐹) = 2) → (𝐹 ∈ Word dom 𝐸 ↔ 𝐹:(0..^2)⟶dom 𝐸)) |
10 | | oveq2 6557 |
. . . . . . . . 9
⊢
((#‘𝐹) = 2
→ (0...(#‘𝐹)) =
(0...2)) |
11 | 10 | feq2d 5944 |
. . . . . . . 8
⊢
((#‘𝐹) = 2
→ (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ 𝑃:(0...2)⟶𝑉)) |
12 | 11 | adantl 481 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) ∧ (#‘𝐹) = 2) → (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ 𝑃:(0...2)⟶𝑉)) |
13 | | fzo0to2pr 12420 |
. . . . . . . . . . 11
⊢ (0..^2) =
{0, 1} |
14 | 4, 13 | syl6eq 2660 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
{0, 1}) |
15 | 14 | raleqdv 3121 |
. . . . . . . . 9
⊢
((#‘𝐹) = 2
→ (∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
16 | | 2wlklem 26094 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
{0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
17 | 15, 16 | syl6bb 275 |
. . . . . . . 8
⊢
((#‘𝐹) = 2
→ (∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) |
18 | 17 | adantl 481 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) ∧ (#‘𝐹) = 2) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) |
19 | 9, 12, 18 | 3anbi123d 1391 |
. . . . . 6
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) ∧ (#‘𝐹) = 2) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ↔ (𝐹:(0..^2)⟶dom 𝐸 ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
20 | | 3anass 1035 |
. . . . . 6
⊢ ((𝐹:(0..^2)⟶dom 𝐸 ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ↔ (𝐹:(0..^2)⟶dom 𝐸 ∧ (𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
21 | 19, 20 | syl6bb 275 |
. . . . 5
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) ∧ (#‘𝐹) = 2) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ↔ (𝐹:(0..^2)⟶dom 𝐸 ∧ (𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))))) |
22 | 21 | ex 449 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → ((#‘𝐹) = 2 → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ↔ (𝐹:(0..^2)⟶dom 𝐸 ∧ (𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))))) |
23 | 22 | pm5.32rd 670 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (#‘𝐹) = 2) ↔ ((𝐹:(0..^2)⟶dom 𝐸 ∧ (𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) ∧ (#‘𝐹) = 2))) |
24 | | 3anass 1035 |
. . . 4
⊢ (((𝐹:(0..^2)⟶dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ↔ ((𝐹:(0..^2)⟶dom 𝐸 ∧ (#‘𝐹) = 2) ∧ (𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
25 | | an32 835 |
. . . 4
⊢ (((𝐹:(0..^2)⟶dom 𝐸 ∧ (#‘𝐹) = 2) ∧ (𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) ↔ ((𝐹:(0..^2)⟶dom 𝐸 ∧ (𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) ∧ (#‘𝐹) = 2)) |
26 | 24, 25 | bitri 263 |
. . 3
⊢ (((𝐹:(0..^2)⟶dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ↔ ((𝐹:(0..^2)⟶dom 𝐸 ∧ (𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) ∧ (#‘𝐹) = 2)) |
27 | 23, 26 | syl6bbr 277 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (#‘𝐹) = 2) ↔ ((𝐹:(0..^2)⟶dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
28 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:(0..^2)⟶dom 𝐸 → 𝐹 Fn (0..^2)) |
29 | | hashfn 13025 |
. . . . . . . 8
⊢ (𝐹 Fn (0..^2) →
(#‘𝐹) =
(#‘(0..^2))) |
30 | | 2nn0 11186 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
31 | | hashfzo0 13077 |
. . . . . . . . 9
⊢ (2 ∈
ℕ0 → (#‘(0..^2)) = 2) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . 8
⊢
(#‘(0..^2)) = 2 |
33 | 29, 32 | syl6eq 2660 |
. . . . . . 7
⊢ (𝐹 Fn (0..^2) →
(#‘𝐹) =
2) |
34 | 28, 33 | syl 17 |
. . . . . 6
⊢ (𝐹:(0..^2)⟶dom 𝐸 → (#‘𝐹) = 2) |
35 | 34 | pm4.71i 662 |
. . . . 5
⊢ (𝐹:(0..^2)⟶dom 𝐸 ↔ (𝐹:(0..^2)⟶dom 𝐸 ∧ (#‘𝐹) = 2)) |
36 | 35 | bicomi 213 |
. . . 4
⊢ ((𝐹:(0..^2)⟶dom 𝐸 ∧ (#‘𝐹) = 2) ↔ 𝐹:(0..^2)⟶dom 𝐸) |
37 | 36 | a1i 11 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → ((𝐹:(0..^2)⟶dom 𝐸 ∧ (#‘𝐹) = 2) ↔ 𝐹:(0..^2)⟶dom 𝐸)) |
38 | 37 | 3anbi1d 1395 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (((𝐹:(0..^2)⟶dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ↔ (𝐹:(0..^2)⟶dom 𝐸 ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
39 | 2, 27, 38 | 3bitrd 293 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2) ↔ (𝐹:(0..^2)⟶dom 𝐸 ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |