Step | Hyp | Ref
| Expression |
1 | | upgr2wlk.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | upgr2wlk.i |
. . . . 5
⊢ 𝐼 = (iEdg‘𝐺) |
3 | 1, 2 | upgriswlk 40849 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
4 | 3 | 3expb 1258 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
5 | 4 | anbi1d 737 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → ((𝐹(1Walks‘𝐺)𝑃 ∧ (#‘𝐹) = 2) ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (#‘𝐹) = 2))) |
6 | | iswrdb 13166 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word dom 𝐼 ↔ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) |
7 | | oveq2 6557 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
(0..^2)) |
8 | 7 | feq2d 5944 |
. . . . . . . . 9
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ↔ 𝐹:(0..^2)⟶dom 𝐼)) |
9 | 6, 8 | syl5bb 271 |
. . . . . . . 8
⊢
((#‘𝐹) = 2
→ (𝐹 ∈ Word dom
𝐼 ↔ 𝐹:(0..^2)⟶dom 𝐼)) |
10 | | oveq2 6557 |
. . . . . . . . 9
⊢
((#‘𝐹) = 2
→ (0...(#‘𝐹)) =
(0...2)) |
11 | 10 | feq2d 5944 |
. . . . . . . 8
⊢
((#‘𝐹) = 2
→ (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ 𝑃:(0...2)⟶𝑉)) |
12 | | fzo0to2pr 12420 |
. . . . . . . . . . 11
⊢ (0..^2) =
{0, 1} |
13 | 7, 12 | syl6eq 2660 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
{0, 1}) |
14 | 13 | raleqdv 3121 |
. . . . . . . . 9
⊢
((#‘𝐹) = 2
→ (∀𝑘 ∈
(0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1} (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
15 | | 2Wlklem 40875 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
{0, 1} (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
16 | 14, 15 | syl6bb 275 |
. . . . . . . 8
⊢
((#‘𝐹) = 2
→ (∀𝑘 ∈
(0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) |
17 | 9, 11, 16 | 3anbi123d 1391 |
. . . . . . 7
⊢
((#‘𝐹) = 2
→ ((𝐹 ∈ Word dom
𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ↔ (𝐹:(0..^2)⟶dom 𝐼 ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
18 | 17 | adantl 481 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) ∧ (#‘𝐹) = 2) → ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ↔ (𝐹:(0..^2)⟶dom 𝐼 ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
19 | | 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)})))) |
20 | 18, 19 | syl6bb 275 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) ∧ (#‘𝐹) = 2) → ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ↔ (𝐹:(0..^2)⟶dom 𝐼 ∧ (𝑃:(0...2)⟶𝑉 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))))) |
21 | 20 | ex 449 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → ((#‘𝐹) = 2 → ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ↔ (𝐹:(0..^2)⟶dom 𝐼 ∧ (𝑃:(0...2)⟶𝑉 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))))) |
22 | 21 | pm5.32rd 670 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (#‘𝐹) = 2) ↔ ((𝐹:(0..^2)⟶dom 𝐼 ∧ (𝑃:(0...2)⟶𝑉 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) ∧ (#‘𝐹) = 2))) |
23 | | 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)})))) |
24 | | 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)) |
25 | 23, 24 | 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)) |
26 | 22, 25 | syl6bbr 277 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (#‘𝐹) = 2) ↔ ((𝐹:(0..^2)⟶dom 𝐼 ∧ (#‘𝐹) = 2) ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
27 | | 2nn0 11186 |
. . . . . . 7
⊢ 2 ∈
ℕ0 |
28 | | fnfzo0hash 13091 |
. . . . . . 7
⊢ ((2
∈ ℕ0 ∧ 𝐹:(0..^2)⟶dom 𝐼) → (#‘𝐹) = 2) |
29 | 27, 28 | mpan 702 |
. . . . . 6
⊢ (𝐹:(0..^2)⟶dom 𝐼 → (#‘𝐹) = 2) |
30 | 29 | pm4.71i 662 |
. . . . 5
⊢ (𝐹:(0..^2)⟶dom 𝐼 ↔ (𝐹:(0..^2)⟶dom 𝐼 ∧ (#‘𝐹) = 2)) |
31 | 30 | bicomi 213 |
. . . 4
⊢ ((𝐹:(0..^2)⟶dom 𝐼 ∧ (#‘𝐹) = 2) ↔ 𝐹:(0..^2)⟶dom 𝐼) |
32 | 31 | a1i 11 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → ((𝐹:(0..^2)⟶dom 𝐼 ∧ (#‘𝐹) = 2) ↔ 𝐹:(0..^2)⟶dom 𝐼)) |
33 | 32 | 3anbi1d 1395 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (((𝐹:(0..^2)⟶dom 𝐼 ∧ (#‘𝐹) = 2) ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ↔ (𝐹:(0..^2)⟶dom 𝐼 ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
34 | 5, 26, 33 | 3bitrd 293 |
1
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → ((𝐹(1Walks‘𝐺)𝑃 ∧ (#‘𝐹) = 2) ↔ (𝐹:(0..^2)⟶dom 𝐼 ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |