| Step | Hyp | Ref
| Expression |
| 1 | | usgrupgr 29202 |
. . . 4
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UPGraph) |
| 2 | | eqid 2737 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 4 | 2, 3 | upgriswlk 29659 |
. . . 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 29685 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
{0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
| 7 | | simplll 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → 𝐺 ∈ USGraph) |
| 8 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢ (𝑃‘0) ∈
V |
| 9 | 3 | usgrnloopv 29217 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USGraph ∧ (𝑃‘0) ∈ V) →
(((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → (𝑃‘0) ≠ (𝑃‘1))) |
| 10 | 7, 8, 9 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → (𝑃‘0) ≠ (𝑃‘1))) |
| 11 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢ (𝑃‘1) ∈
V |
| 12 | 3 | usgrnloopv 29217 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USGraph ∧ (𝑃‘1) ∈ V) →
(((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘1) ≠ (𝑃‘2))) |
| 13 | 7, 11, 12 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘1) ≠ (𝑃‘2))) |
| 14 | 10, 13 | anim12d 609 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)))) |
| 15 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘0) = (𝐹‘1) → (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ↔ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)})) |
| 16 | | eqtr2 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → {(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)}) |
| 17 | | prcom 4732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ {(𝑃‘1), (𝑃‘2)} = {(𝑃‘2), (𝑃‘1)} |
| 18 | 17 | eqeq2i 2750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)} ↔ {(𝑃‘0), (𝑃‘1)} = {(𝑃‘2), (𝑃‘1)}) |
| 19 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃‘2) ∈
V |
| 20 | 8, 19 | preqr1 4848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({(𝑃‘0), (𝑃‘1)} = {(𝑃‘2), (𝑃‘1)} → (𝑃‘0) = (𝑃‘2)) |
| 21 | 18, 20 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) = (𝑃‘2)) |
| 22 | 16, 21 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) = (𝑃‘2)) |
| 23 | 22 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)} → (((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) = (𝑃‘2))) |
| 24 | 15, 23 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘0) = (𝐹‘1) → (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → (((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) = (𝑃‘2)))) |
| 25 | 24 | impd 410 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘0) = (𝐹‘1) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) = (𝑃‘2))) |
| 26 | 25 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((𝐹‘0) = (𝐹‘1) → (𝑃‘0) = (𝑃‘2))) |
| 27 | 26 | necon3d 2961 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((𝑃‘0) ≠ (𝑃‘2) → (𝐹‘0) ≠ (𝐹‘1))) |
| 28 | 27 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘0) ≠ (𝑃‘2) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐹‘0) ≠ (𝐹‘1))) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐹‘0) ≠ (𝐹‘1))) |
| 30 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) → (𝑃‘0) ≠ (𝑃‘1)) |
| 31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → (𝑃‘0) ≠ (𝑃‘1)) |
| 32 | | simpl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → (𝑃‘0) ≠ (𝑃‘2)) |
| 33 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → (𝑃‘1) ≠ (𝑃‘2)) |
| 34 | 31, 32, 33 | 3jca 1129 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2))) |
| 35 | 29, 34 | jctild 525 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
| 36 | 35 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃‘0) ≠ (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
| 37 | 36 | 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))))) |
| 38 | 37 | adantl 481 |
. . . . . . . . . . . . . 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))))) |
| 39 | 38 | adantr 480 |
. . . . . . . . . . . . 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))))) |
| 40 | 14, 39 | 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)))) |
| 41 | 6, 40 | biimtrid 242 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) ∧ 𝑃:(0...2)⟶(Vtx‘𝐺)) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
| 42 | 41 | ex 412 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) → (𝑃:(0...2)⟶(Vtx‘𝐺) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
| 43 | 42 | com23 86 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝑃‘0) ≠ (𝑃‘2)) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
| 44 | 43 | ex 412 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
((𝑃‘0) ≠ (𝑃‘2) → (∀𝑘 ∈ {0, 1}
((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
| 45 | | fveq2 6906 |
. . . . . . . . . 10
⊢
((♯‘𝐹) =
2 → (𝑃‘(♯‘𝐹)) = (𝑃‘2)) |
| 46 | 45 | neeq2d 3001 |
. . . . . . . . 9
⊢
((♯‘𝐹) =
2 → ((𝑃‘0) ≠
(𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) ≠ (𝑃‘2))) |
| 47 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
2 → (0..^(♯‘𝐹)) = (0..^2)) |
| 48 | | fzo0to2pr 13789 |
. . . . . . . . . . . 12
⊢ (0..^2) =
{0, 1} |
| 49 | 47, 48 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢
((♯‘𝐹) =
2 → (0..^(♯‘𝐹)) = {0, 1}) |
| 50 | 49 | raleqdv 3326 |
. . . . . . . . . 10
⊢
((♯‘𝐹) =
2 → (∀𝑘 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 51 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
2 → (0...(♯‘𝐹)) = (0...2)) |
| 52 | 51 | feq2d 6722 |
. . . . . . . . . . 11
⊢
((♯‘𝐹) =
2 → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ↔ 𝑃:(0...2)⟶(Vtx‘𝐺))) |
| 53 | 52 | imbi1d 341 |
. . . . . . . . . 10
⊢
((♯‘𝐹) =
2 → ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))) ↔ (𝑃:(0...2)⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
| 54 | 50, 53 | imbi12d 344 |
. . . . . . . . 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)))))) |
| 55 | 46, 54 | imbi12d 344 |
. . . . . . . 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))))))) |
| 56 | 44, 55 | syl5ibrcom 247 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
((♯‘𝐹) = 2
→ ((𝑃‘0) ≠
(𝑃‘(♯‘𝐹)) → (∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))))) |
| 57 | 56 | impd 410 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
(((♯‘𝐹) = 2
∧ (𝑃‘0) ≠
(𝑃‘(♯‘𝐹))) → (∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
| 58 | 57 | com24 95 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
(𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → (∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))))) |
| 59 | 58 | ex 412 |
. . . 4
⊢ (𝐺 ∈ USGraph → (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → (∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (((♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))))) |
| 60 | 59 | 3impd 1349 |
. . 3
⊢ (𝐺 ∈ USGraph → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (((♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
| 61 | 5, 60 | sylbid 240 |
. 2
⊢ (𝐺 ∈ USGraph → (𝐹(Walks‘𝐺)𝑃 → (((♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))))) |
| 62 | 61 | imp31 417 |
1
⊢ (((𝐺 ∈ USGraph ∧ 𝐹(Walks‘𝐺)𝑃) ∧ ((♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))) |