Step | Hyp | Ref
| Expression |
1 | | usgrupgr 26077 |
. . . 4
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph
) |
2 | | eqid 2622 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2622 |
. . . . 5
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
4 | 2, 3 | upgriswlk 26537 |
. . . 4
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
5 | 1, 4 | syl 17 |
. . 3
⊢ (𝐺 ∈ USGraph → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
6 | | 2wlklem 26563 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
{0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
7 | | simplll 798 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → 𝐺 ∈ USGraph ) |
8 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢ (𝑃‘0) ∈
V |
9 | 3 | usgrnloopv 26092 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USGraph ∧ (𝑃‘0) ∈ V) →
(((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → (𝑃‘0) ≠ (𝑃‘1))) |
10 | 7, 8, 9 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → (𝑃‘0) ≠ (𝑃‘1))) |
11 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢ (𝑃‘1) ∈
V |
12 | 3 | usgrnloopv 26092 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USGraph ∧ (𝑃‘1) ∈ V) →
(((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘1) ≠ (𝑃‘2))) |
13 | 7, 11, 12 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘1) ≠ (𝑃‘2))) |
14 | 10, 13 | anim12d 586 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)))) |
15 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹‘0) = (𝐹‘1) → ((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1))) |
16 | 15 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘0) = (𝐹‘1) → (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ↔ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)})) |
17 | | eqtr2 2642 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → {(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)}) |
18 | | prcom 4267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ {(𝑃‘1), (𝑃‘2)} = {(𝑃‘2), (𝑃‘1)} |
19 | 18 | eqeq2i 2634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)} ↔ {(𝑃‘0), (𝑃‘1)} = {(𝑃‘2), (𝑃‘1)}) |
20 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃‘2) ∈
V |
21 | 8, 20 | preqr1 4379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({(𝑃‘0), (𝑃‘1)} = {(𝑃‘2), (𝑃‘1)} → (𝑃‘0) = (𝑃‘2)) |
22 | 19, 21 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) = (𝑃‘2)) |
23 | 17, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) = (𝑃‘2)) |
24 | 23 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)} → (((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) = (𝑃‘2))) |
25 | 16, 24 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘0) = (𝐹‘1) → (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → (((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) = (𝑃‘2)))) |
26 | 25 | impd 447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘0) = (𝐹‘1) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) = (𝑃‘2))) |
27 | 26 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((𝐹‘0) = (𝐹‘1) → (𝑃‘0) = (𝑃‘2))) |
28 | 27 | necon3d 2815 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((𝑃‘0) ≠ (𝑃‘2) → (𝐹‘0) ≠ (𝐹‘1))) |
29 | 28 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘0) ≠ (𝑃‘2) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐹‘0) ≠ (𝐹‘1))) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐹‘0) ≠ (𝐹‘1))) |
31 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) → (𝑃‘0) ≠ (𝑃‘1)) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → (𝑃‘0) ≠ (𝑃‘1)) |
33 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → (𝑃‘0) ≠ (𝑃‘2)) |
34 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → (𝑃‘1) ≠ (𝑃‘2)) |
35 | 32, 33, 34 | 3jca 1242 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2))) |
36 | 30, 35 | jctild 566 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
37 | 36 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃‘0) ≠ (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
38 | 37 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃‘0) ≠ (𝑃‘2) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
39 | 38 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
40 | 39 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
41 | 14, 40 | mpdd 43 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
42 | 6, 41 | syl5bi 232 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
43 | 42 | ex 450 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) → (𝑃:(0...2)⟶(Vtx‘𝐺) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
44 | 43 | com23 86 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
45 | 44 | ex 450 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
((𝑃‘0) ≠ (𝑃‘2) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
46 | | fveq2 6191 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ (𝑃‘(#‘𝐹)) = (𝑃‘2)) |
47 | 46 | neeq2d 2854 |
. . . . . . . . 9
⊢
((#‘𝐹) = 2
→ ((𝑃‘0) ≠
(𝑃‘(#‘𝐹)) ↔ (𝑃‘0) ≠ (𝑃‘2))) |
48 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
(0..^2)) |
49 | | fzo0to2pr 12553 |
. . . . . . . . . . . 12
⊢ (0..^2) =
{0, 1} |
50 | 48, 49 | syl6eq 2672 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
{0, 1}) |
51 | 50 | raleqdv 3144 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ (∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
52 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 2
→ (0...(#‘𝐹)) =
(0...2)) |
53 | 52 | feq2d 6031 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 2
→ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ↔ 𝑃:(0...2)⟶(Vtx‘𝐺))) |
54 | 53 | imbi1d 331 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))) ↔ (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
55 | 51, 54 | imbi12d 334 |
. . . . . . . . 9
⊢
((#‘𝐹) = 2
→ ((∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))) ↔ (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
56 | 47, 55 | imbi12d 334 |
. . . . . . . 8
⊢
((#‘𝐹) = 2
→ (((𝑃‘0) ≠
(𝑃‘(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) ↔ ((𝑃‘0) ≠ (𝑃‘2) → (∀𝑘 ∈ {0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))))) |
57 | 45, 56 | syl5ibrcom 237 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
((#‘𝐹) = 2 →
((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))))) |
58 | 57 | impd 447 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
(((#‘𝐹) = 2 ∧
(𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
59 | 58 | com24 95 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
(𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
60 | 59 | ex 450 |
. . . 4
⊢ (𝐺 ∈ USGraph → (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))))) |
61 | 60 | 3impd 1281 |
. . 3
⊢ (𝐺 ∈ USGraph → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
62 | 5, 61 | sylbid 230 |
. 2
⊢ (𝐺 ∈ USGraph → (𝐹(Walks‘𝐺)𝑃 → (((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
63 | 62 | imp31 448 |
1
⊢ (((𝐺 ∈ USGraph ∧ 𝐹(Walks‘𝐺)𝑃) ∧ ((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))) |