Proof of Theorem 2pthnloop
Step | Hyp | Ref
| Expression |
1 | | pthis1wlk 40933 |
. . . . 5
⊢ (𝐹(PathS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
2 | | wlkv 40815 |
. . . . 5
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐹(PathS‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
4 | | isPth 40929 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(PathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
5 | | isTrl 40904 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(TrailS‘𝐺)𝑃 ↔ (𝐹(1Walks‘𝐺)𝑃 ∧ Fun ◡𝐹))) |
6 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
7 | | 2pthnloop.i |
. . . . . . . . . . . . 13
⊢ 𝐼 = (iEdg‘𝐺) |
8 | 6, 7 | is1wlk 40813 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))) |
9 | 8 | anbi1d 737 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → ((𝐹(1Walks‘𝐺)𝑃 ∧ Fun ◡𝐹) ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ∧ Fun ◡𝐹))) |
10 | 5, 9 | bitrd 267 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(TrailS‘𝐺)𝑃 ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ∧ Fun ◡𝐹))) |
11 | | pthdadjvtx 40936 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (𝑃‘𝑖) ≠ (𝑃‘(𝑖 + 1))) |
12 | 11 | ad5ant245 1299 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(PathS‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (𝑃‘𝑖) ≠ (𝑃‘(𝑖 + 1))) |
13 | 12 | neneqd 2787 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(PathS‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → ¬ (𝑃‘𝑖) = (𝑃‘(𝑖 + 1))) |
14 | | ifpfal 1018 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) |
15 | 14 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(PathS‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) ∧ ¬ (𝑃‘𝑖) = (𝑃‘(𝑖 + 1))) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) |
16 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃‘𝑖) ∈ V |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → (𝑃‘𝑖) ∈ V) |
18 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃‘(𝑖 + 1)) ∈ V |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → (𝑃‘(𝑖 + 1)) ∈ V) |
20 | | neqne 2790 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → (𝑃‘𝑖) ≠ (𝑃‘(𝑖 + 1))) |
21 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐼‘(𝐹‘𝑖)) ∈ V |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → (𝐼‘(𝐹‘𝑖)) ∈ V) |
23 | | prsshashgt1 13059 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃‘𝑖) ∈ V ∧ (𝑃‘(𝑖 + 1)) ∈ V ∧ (𝑃‘𝑖) ≠ (𝑃‘(𝑖 + 1))) ∧ (𝐼‘(𝐹‘𝑖)) ∈ V) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)) → 2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
24 | 17, 19, 20, 22, 23 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)) → 2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(PathS‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) ∧ ¬ (𝑃‘𝑖) = (𝑃‘(𝑖 + 1))) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)) → 2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
26 | 15, 25 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(PathS‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) ∧ ¬ (𝑃‘𝑖) = (𝑃‘(𝑖 + 1))) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → 2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
27 | 13, 26 | mpdan 699 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(PathS‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → 2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
28 | 27 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(PathS‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
29 | 28 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(PathS‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) → (1 < (#‘𝐹) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))) |
30 | 29 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(PathS‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))) |
31 | 30 | exp31 628 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (𝐹(PathS‘𝐺)𝑃 → (((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))))) |
32 | 31 | com24 93 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → (((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))))) |
33 | 32 | 3impia 1253 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))) |
34 | 33 | exp4c 634 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (Fun ◡𝐹 → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))))) |
35 | 34 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ∧ Fun ◡𝐹) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))))) |
36 | 35 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ∧ Fun ◡𝐹) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))))) |
37 | 10, 36 | sylbid 229 |
. . . . . . . . 9
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(TrailS‘𝐺)𝑃 → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))))) |
38 | 37 | com24 93 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (𝐹(TrailS‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))))) |
39 | 38 | com14 94 |
. . . . . . 7
⊢ (𝐹(TrailS‘𝐺)𝑃 → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))))) |
40 | 39 | 3imp 1249 |
. . . . . 6
⊢ ((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))) |
41 | 40 | com12 32 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → ((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))) |
42 | 4, 41 | sylbid 229 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(PathS‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))) |
43 | 3, 42 | mpcom 37 |
. . 3
⊢ (𝐹(PathS‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))) |
44 | 43 | pm2.43i 50 |
. 2
⊢ (𝐹(PathS‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
45 | 44 | imp 444 |
1
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹)) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))) |