Proof of Theorem 2pthnloop
Step | Hyp | Ref
| Expression |
1 | | pthiswlk 26623 |
. . . . 5
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) |
2 | | wlkv 26508 |
. . . . 5
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
4 | | ispth 26619 |
. . . . . . 7
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅)) |
5 | 4 | a1i 11 |
. . . . . 6
⊢ (𝐺 ∈ V → (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
6 | | istrl 26593 |
. . . . . . . . . . . 12
⊢ (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝐹)) |
7 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
8 | | 2pthnloop.i |
. . . . . . . . . . . . . 14
⊢ 𝐼 = (iEdg‘𝐺) |
9 | 7, 8 | iswlkg 26509 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ V → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))) |
10 | 9 | anbi1d 741 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ V → ((𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝐹) ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ∧ Fun ◡𝐹))) |
11 | 6, 10 | syl5bb 272 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ V → (𝐹(Trails‘𝐺)𝑃 ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ∧ Fun ◡𝐹))) |
12 | | pthdadjvtx 26626 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (𝑃‘𝑖) ≠ (𝑃‘(𝑖 + 1))) |
13 | 12 | ad5ant245 1307 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (𝑃‘𝑖) ≠ (𝑃‘(𝑖 + 1))) |
14 | 13 | neneqd 2799 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → ¬ (𝑃‘𝑖) = (𝑃‘(𝑖 + 1))) |
15 | | ifpfal 1024 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) |
16 | 15 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) ∧ ¬ (𝑃‘𝑖) = (𝑃‘(𝑖 + 1))) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) |
17 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → (𝑃‘𝑖) ∈ V) |
18 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → (𝑃‘(𝑖 + 1)) ∈ V) |
19 | | neqne 2802 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → (𝑃‘𝑖) ≠ (𝑃‘(𝑖 + 1))) |
20 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → (𝐼‘(𝐹‘𝑖)) ∈ V) |
21 | | prsshashgt1 13198 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑃‘𝑖) ∈ V ∧ (𝑃‘(𝑖 + 1)) ∈ V ∧ (𝑃‘𝑖) ≠ (𝑃‘(𝑖 + 1))) ∧ (𝐼‘(𝐹‘𝑖)) ∈ V) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)) → 2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
22 | 17, 18, 19, 20, 21 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
(𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)) → 2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) ∧ ¬ (𝑃‘𝑖) = (𝑃‘(𝑖 + 1))) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)) → 2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
24 | 16, 23 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) ∧ ¬ (𝑃‘𝑖) = (𝑃‘(𝑖 + 1))) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → 2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
25 | 14, 24 | mpdan 702 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → 2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
26 | 25 | ralimdva 2962 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈ Word
dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) ∧ 1 < (#‘𝐹)) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
27 | 26 | ex 450 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) → (1 < (#‘𝐹) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))) |
28 | 27 | com23 86 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))) |
29 | 28 | exp31 630 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (𝐹(Paths‘𝐺)𝑃 → (((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))))) |
30 | 29 | com24 95 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → (((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))))) |
31 | 30 | 3impia 1261 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (((Fun ◡𝐹 ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))) |
32 | 31 | exp4c 636 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (Fun ◡𝐹 → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))))) |
33 | 32 | imp 445 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ∧ Fun ◡𝐹) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))))) |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ V → (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ∧ Fun ◡𝐹) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))))) |
35 | 11, 34 | sylbid 230 |
. . . . . . . . . 10
⊢ (𝐺 ∈ V → (𝐹(Trails‘𝐺)𝑃 → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))))) |
36 | 35 | com24 95 |
. . . . . . . . 9
⊢ (𝐺 ∈ V → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (𝐹(Trails‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))))) |
37 | 36 | com14 96 |
. . . . . . . 8
⊢ (𝐹(Trails‘𝐺)𝑃 → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (𝐺 ∈ V → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))))) |
38 | 37 | 3imp 1256 |
. . . . . . 7
⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝐺 ∈ V → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))) |
39 | 38 | com12 32 |
. . . . . 6
⊢ (𝐺 ∈ V → ((𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))) |
40 | 5, 39 | sylbid 230 |
. . . . 5
⊢ (𝐺 ∈ V → (𝐹(Paths‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))) |
41 | 40 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Paths‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))))) |
42 | 3, 41 | mpcom 38 |
. . 3
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))))) |
43 | 42 | pm2.43i 52 |
. 2
⊢ (𝐹(Paths‘𝐺)𝑃 → (1 < (#‘𝐹) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖))))) |
44 | 43 | imp 445 |
1
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹)) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))) |