Proof of Theorem pthdivtx
Step | Hyp | Ref
| Expression |
1 | | pthis1wlk 40933 |
. . . 4
⊢ (𝐹(PathS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
2 | | wlkv 40815 |
. . . 4
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝐹(PathS‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
4 | | isPth 40929 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(PathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
5 | | trlis1wlk 40905 |
. . . . . 6
⊢ (𝐹(TrailS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
6 | | eqid 2610 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
7 | 6 | 1wlkp 40821 |
. . . . . 6
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) |
8 | | elfz0lmr 40367 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (0...(#‘𝐹)) → (𝐽 = 0 ∨ 𝐽 ∈ (1..^(#‘𝐹)) ∨ 𝐽 = (#‘𝐹))) |
9 | | elfzo1 12385 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∈ (1..^(#‘𝐹)) ↔ (𝐼 ∈ ℕ ∧ (#‘𝐹) ∈ ℕ ∧ 𝐼 < (#‘𝐹))) |
10 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝐹) ∈
ℕ → (#‘𝐹)
∈ ℕ0) |
11 | 10 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈ ℕ ∧
(#‘𝐹) ∈ ℕ
∧ 𝐼 < (#‘𝐹)) → (#‘𝐹) ∈
ℕ0) |
12 | 9, 11 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈ (1..^(#‘𝐹)) → (#‘𝐹) ∈
ℕ0) |
13 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (#‘𝐹) ∈
ℕ0) |
14 | | fvinim0ffz 12449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (#‘𝐹) ∈ ℕ0) →
(((𝑃 “ {0,
(#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ ↔ ((𝑃‘0) ∉ (𝑃 “ (1..^(#‘𝐹))) ∧ (𝑃‘(#‘𝐹)) ∉ (𝑃 “ (1..^(#‘𝐹)))))) |
15 | 13, 14 | sylan2 490 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ ↔ ((𝑃‘0) ∉ (𝑃 “ (1..^(#‘𝐹))) ∧ (𝑃‘(#‘𝐹)) ∉ (𝑃 “ (1..^(#‘𝐹)))))) |
16 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐽 = 0 → (𝑃‘𝐽) = (𝑃‘0)) |
17 | 16 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐽 = 0 → ((𝑃‘𝐼) = (𝑃‘𝐽) ↔ (𝑃‘𝐼) = (𝑃‘0))) |
18 | 17 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘𝐼) = (𝑃‘𝐽) ↔ (𝑃‘𝐼) = (𝑃‘0))) |
19 | | ffun 5961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → Fun 𝑃) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → Fun 𝑃) |
21 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → dom 𝑃 = (0...(#‘𝐹))) |
22 | | fzo0ss1 12367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(1..^(#‘𝐹))
⊆ (0..^(#‘𝐹)) |
23 | | fzossfz 12357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(0..^(#‘𝐹))
⊆ (0...(#‘𝐹)) |
24 | 22, 23 | sstri 3577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(1..^(#‘𝐹))
⊆ (0...(#‘𝐹)) |
25 | 24 | sseli 3564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐼 ∈ (1..^(#‘𝐹)) → 𝐼 ∈ (0...(#‘𝐹))) |
26 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (dom
𝑃 = (0...(#‘𝐹)) → (𝐼 ∈ dom 𝑃 ↔ 𝐼 ∈ (0...(#‘𝐹)))) |
27 | 25, 26 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (dom
𝑃 = (0...(#‘𝐹)) → (𝐼 ∈ (1..^(#‘𝐹)) → 𝐼 ∈ dom 𝑃)) |
28 | 21, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (𝐼 ∈ (1..^(#‘𝐹)) → 𝐼 ∈ dom 𝑃)) |
29 | 28 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → 𝐼 ∈ dom 𝑃) |
30 | 20, 29 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (Fun 𝑃 ∧ 𝐼 ∈ dom 𝑃)) |
31 | 30 | adantrl 748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (Fun 𝑃 ∧ 𝐼 ∈ dom 𝑃)) |
32 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → 𝐼 ∈ (1..^(#‘𝐹))) |
33 | | funfvima 6396 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Fun
𝑃 ∧ 𝐼 ∈ dom 𝑃) → (𝐼 ∈ (1..^(#‘𝐹)) → (𝑃‘𝐼) ∈ (𝑃 “ (1..^(#‘𝐹))))) |
34 | 31, 32, 33 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (𝑃‘𝐼) ∈ (𝑃 “ (1..^(#‘𝐹)))) |
35 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃‘𝐼) = (𝑃‘0) → ((𝑃‘𝐼) ∈ (𝑃 “ (1..^(#‘𝐹))) ↔ (𝑃‘0) ∈ (𝑃 “ (1..^(#‘𝐹))))) |
36 | 34, 35 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘𝐼) = (𝑃‘0) → (𝑃‘0) ∈ (𝑃 “ (1..^(#‘𝐹))))) |
37 | 18, 36 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘𝐼) = (𝑃‘𝐽) → (𝑃‘0) ∈ (𝑃 “ (1..^(#‘𝐹))))) |
38 | | nnel 2892 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
(𝑃‘0) ∉ (𝑃 “ (1..^(#‘𝐹))) ↔ (𝑃‘0) ∈ (𝑃 “ (1..^(#‘𝐹)))) |
39 | 37, 38 | syl6ibr 241 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘𝐼) = (𝑃‘𝐽) → ¬ (𝑃‘0) ∉ (𝑃 “ (1..^(#‘𝐹))))) |
40 | 39 | necon2ad 2797 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘0) ∉ (𝑃 “ (1..^(#‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
41 | 40 | adantrd 483 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (((𝑃‘0) ∉ (𝑃 “ (1..^(#‘𝐹))) ∧ (𝑃‘(#‘𝐹)) ∉ (𝑃 “ (1..^(#‘𝐹)))) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
42 | 15, 41 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
43 | 42 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → ((𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (𝑃‘𝐼) ≠ (𝑃‘𝐽)))) |
44 | 43 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → ((𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘𝐽)))) |
45 | 44 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → ((𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))))) |
46 | 45 | 3imp 1249 |
. . . . . . . . . . . . . 14
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → ((𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
47 | 46 | com12 32 |
. . . . . . . . . . . . 13
⊢ ((𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹))) → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
48 | 47 | a1d 25 |
. . . . . . . . . . . 12
⊢ ((𝐽 = 0 ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (𝐼 ≠ 𝐽 → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃‘𝐼) ≠ (𝑃‘𝐽)))) |
49 | 48 | ex 449 |
. . . . . . . . . . 11
⊢ (𝐽 = 0 → (𝐼 ∈ (1..^(#‘𝐹)) → (𝐼 ≠ 𝐽 → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))))) |
50 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈ (1..^(#‘𝐹)) → ((𝑃 ↾ (1..^(#‘𝐹)))‘𝐼) = (𝑃‘𝐼)) |
51 | 50 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → ((𝑃 ↾ (1..^(#‘𝐹)))‘𝐼) = (𝑃‘𝐼)) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃 ↾ (1..^(#‘𝐹)))‘𝐼) = (𝑃‘𝐼)) |
53 | 52 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (𝑃‘𝐼) = ((𝑃 ↾ (1..^(#‘𝐹)))‘𝐼)) |
54 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐽 ∈ (1..^(#‘𝐹)) → ((𝑃 ↾ (1..^(#‘𝐹)))‘𝐽) = (𝑃‘𝐽)) |
55 | 54 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃 ↾ (1..^(#‘𝐹)))‘𝐽) = (𝑃‘𝐽)) |
56 | 55 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (𝑃‘𝐽) = ((𝑃 ↾ (1..^(#‘𝐹)))‘𝐽)) |
57 | 53, 56 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘𝐼) = (𝑃‘𝐽) ↔ ((𝑃 ↾ (1..^(#‘𝐹)))‘𝐼) = ((𝑃 ↾ (1..^(#‘𝐹)))‘𝐽))) |
58 | | fssres 5983 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (1..^(#‘𝐹)) ⊆ (0...(#‘𝐹))) → (𝑃 ↾ (1..^(#‘𝐹))):(1..^(#‘𝐹))⟶(Vtx‘𝐺)) |
59 | 24, 58 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (𝑃 ↾ (1..^(#‘𝐹))):(1..^(#‘𝐹))⟶(Vtx‘𝐺)) |
60 | | df-f1 5809 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ↾ (1..^(#‘𝐹))):(1..^(#‘𝐹))–1-1→(Vtx‘𝐺) ↔ ((𝑃 ↾ (1..^(#‘𝐹))):(1..^(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) |
61 | 60 | biimpri 217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ↾ (1..^(#‘𝐹))):(1..^(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) → (𝑃 ↾ (1..^(#‘𝐹))):(1..^(#‘𝐹))–1-1→(Vtx‘𝐺)) |
62 | 59, 61 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) → (𝑃 ↾ (1..^(#‘𝐹))):(1..^(#‘𝐹))–1-1→(Vtx‘𝐺)) |
63 | 62 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃 ↾ (1..^(#‘𝐹))):(1..^(#‘𝐹))–1-1→(Vtx‘𝐺)) |
64 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) |
65 | 64 | ancomd 466 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (𝐼 ∈ (1..^(#‘𝐹)) ∧ 𝐽 ∈ (1..^(#‘𝐹)))) |
66 | | f1veqaeq 6418 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ↾ (1..^(#‘𝐹))):(1..^(#‘𝐹))–1-1→(Vtx‘𝐺) ∧ (𝐼 ∈ (1..^(#‘𝐹)) ∧ 𝐽 ∈ (1..^(#‘𝐹)))) → (((𝑃 ↾ (1..^(#‘𝐹)))‘𝐼) = ((𝑃 ↾ (1..^(#‘𝐹)))‘𝐽) → 𝐼 = 𝐽)) |
67 | 63, 65, 66 | syl2an2r 872 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (((𝑃 ↾ (1..^(#‘𝐹)))‘𝐼) = ((𝑃 ↾ (1..^(#‘𝐹)))‘𝐽) → 𝐼 = 𝐽)) |
68 | 57, 67 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘𝐼) = (𝑃‘𝐽) → 𝐼 = 𝐽)) |
69 | 68 | ancoms 468 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹))) ∧ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅)) → ((𝑃‘𝐼) = (𝑃‘𝐽) → 𝐼 = 𝐽)) |
70 | 69 | necon3d 2803 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹))) ∧ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅)) → (𝐼 ≠ 𝐽 → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
71 | 70 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝐼 ≠ 𝐽 → (𝑃‘𝐼) ≠ (𝑃‘𝐽)))) |
72 | 71 | com23 84 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (1..^(#‘𝐹)) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (𝐼 ≠ 𝐽 → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃‘𝐼) ≠ (𝑃‘𝐽)))) |
73 | 72 | ex 449 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (1..^(#‘𝐹)) → (𝐼 ∈ (1..^(#‘𝐹)) → (𝐼 ≠ 𝐽 → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))))) |
74 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (#‘𝐹) ∈
ℕ0) |
75 | 74, 14 | sylan2 490 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ ↔ ((𝑃‘0) ∉ (𝑃 “ (1..^(#‘𝐹))) ∧ (𝑃‘(#‘𝐹)) ∉ (𝑃 “ (1..^(#‘𝐹)))))) |
76 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐽 = (#‘𝐹) → (𝑃‘𝐽) = (𝑃‘(#‘𝐹))) |
77 | 76 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐽 = (#‘𝐹) → ((𝑃‘𝐼) = (𝑃‘𝐽) ↔ (𝑃‘𝐼) = (𝑃‘(#‘𝐹)))) |
78 | 77 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘𝐼) = (𝑃‘𝐽) ↔ (𝑃‘𝐼) = (𝑃‘(#‘𝐹)))) |
79 | 30 | adantrl 748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (Fun 𝑃 ∧ 𝐼 ∈ dom 𝑃)) |
80 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → 𝐼 ∈ (1..^(#‘𝐹))) |
81 | 79, 80, 33 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (𝑃‘𝐼) ∈ (𝑃 “ (1..^(#‘𝐹)))) |
82 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃‘𝐼) = (𝑃‘(#‘𝐹)) → ((𝑃‘𝐼) ∈ (𝑃 “ (1..^(#‘𝐹))) ↔ (𝑃‘(#‘𝐹)) ∈ (𝑃 “ (1..^(#‘𝐹))))) |
83 | 81, 82 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘𝐼) = (𝑃‘(#‘𝐹)) → (𝑃‘(#‘𝐹)) ∈ (𝑃 “ (1..^(#‘𝐹))))) |
84 | 78, 83 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘𝐼) = (𝑃‘𝐽) → (𝑃‘(#‘𝐹)) ∈ (𝑃 “ (1..^(#‘𝐹))))) |
85 | | nnel 2892 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
(𝑃‘(#‘𝐹)) ∉ (𝑃 “ (1..^(#‘𝐹))) ↔ (𝑃‘(#‘𝐹)) ∈ (𝑃 “ (1..^(#‘𝐹)))) |
86 | 84, 85 | syl6ibr 241 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘𝐼) = (𝑃‘𝐽) → ¬ (𝑃‘(#‘𝐹)) ∉ (𝑃 “ (1..^(#‘𝐹))))) |
87 | 86 | necon2ad 2797 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → ((𝑃‘(#‘𝐹)) ∉ (𝑃 “ (1..^(#‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
88 | 87 | adantld 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (((𝑃‘0) ∉ (𝑃 “ (1..^(#‘𝐹))) ∧ (𝑃‘(#‘𝐹)) ∉ (𝑃 “ (1..^(#‘𝐹)))) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
89 | 75, 88 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ (𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹)))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
90 | 89 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → ((𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → (𝑃‘𝐼) ≠ (𝑃‘𝐽)))) |
91 | 90 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → ((𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘𝐽)))) |
92 | 91 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → ((𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))))) |
93 | 92 | 3imp 1249 |
. . . . . . . . . . . . . 14
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → ((𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
94 | 93 | com12 32 |
. . . . . . . . . . . . 13
⊢ ((𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
95 | 94 | a1d 25 |
. . . . . . . . . . . 12
⊢ ((𝐽 = (#‘𝐹) ∧ 𝐼 ∈ (1..^(#‘𝐹))) → (𝐼 ≠ 𝐽 → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃‘𝐼) ≠ (𝑃‘𝐽)))) |
96 | 95 | ex 449 |
. . . . . . . . . . 11
⊢ (𝐽 = (#‘𝐹) → (𝐼 ∈ (1..^(#‘𝐹)) → (𝐼 ≠ 𝐽 → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))))) |
97 | 49, 73, 96 | 3jaoi 1383 |
. . . . . . . . . 10
⊢ ((𝐽 = 0 ∨ 𝐽 ∈ (1..^(#‘𝐹)) ∨ 𝐽 = (#‘𝐹)) → (𝐼 ∈ (1..^(#‘𝐹)) → (𝐼 ≠ 𝐽 → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))))) |
98 | 8, 97 | syl 17 |
. . . . . . . . 9
⊢ (𝐽 ∈ (0...(#‘𝐹)) → (𝐼 ∈ (1..^(#‘𝐹)) → (𝐼 ≠ 𝐽 → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))))) |
99 | 98 | 3imp21 1269 |
. . . . . . . 8
⊢ ((𝐼 ∈ (1..^(#‘𝐹)) ∧ 𝐽 ∈ (0...(#‘𝐹)) ∧ 𝐼 ≠ 𝐽) → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
100 | 99 | com12 32 |
. . . . . . 7
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → ((𝐼 ∈ (1..^(#‘𝐹)) ∧ 𝐽 ∈ (0...(#‘𝐹)) ∧ 𝐼 ≠ 𝐽) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
101 | 100 | 3exp 1256 |
. . . . . 6
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → ((𝐼 ∈ (1..^(#‘𝐹)) ∧ 𝐽 ∈ (0...(#‘𝐹)) ∧ 𝐼 ≠ 𝐽) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))))) |
102 | 5, 7, 101 | 3syl 18 |
. . . . 5
⊢ (𝐹(TrailS‘𝐺)𝑃 → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → ((𝐼 ∈ (1..^(#‘𝐹)) ∧ 𝐽 ∈ (0...(#‘𝐹)) ∧ 𝐼 ≠ 𝐽) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))))) |
103 | 102 | 3imp 1249 |
. . . 4
⊢ ((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → ((𝐼 ∈ (1..^(#‘𝐹)) ∧ 𝐽 ∈ (0...(#‘𝐹)) ∧ 𝐼 ≠ 𝐽) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
104 | 4, 103 | syl6bi 242 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(PathS‘𝐺)𝑃 → ((𝐼 ∈ (1..^(#‘𝐹)) ∧ 𝐽 ∈ (0...(#‘𝐹)) ∧ 𝐼 ≠ 𝐽) → (𝑃‘𝐼) ≠ (𝑃‘𝐽)))) |
105 | 3, 104 | mpcom 37 |
. 2
⊢ (𝐹(PathS‘𝐺)𝑃 → ((𝐼 ∈ (1..^(#‘𝐹)) ∧ 𝐽 ∈ (0...(#‘𝐹)) ∧ 𝐼 ≠ 𝐽) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))) |
106 | 105 | imp 444 |
1
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝐼 ∈ (1..^(#‘𝐹)) ∧ 𝐽 ∈ (0...(#‘𝐹)) ∧ 𝐼 ≠ 𝐽)) → (𝑃‘𝐼) ≠ (𝑃‘𝐽)) |