Step | Hyp | Ref
| Expression |
1 | | df-spth 26039 |
. . 3
⊢ SPaths =
(𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Trails 𝑒)𝑝 ∧ Fun ◡𝑝)}) |
2 | 1 | brovmpt2ex 7236 |
. 2
⊢ (𝐹(𝑉 SPaths 𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
3 | | simprl 790 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)) → 𝐹(𝑉 Trails 𝐸)𝑃) |
4 | | funres11 5880 |
. . . . . . 7
⊢ (Fun
◡𝑃 → Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) |
5 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃) → Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) |
6 | 5 | adantl 481 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)) → Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) |
7 | | trliswlk 26069 |
. . . . . . . . . 10
⊢ (𝐹(𝑉 Trails 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃)) |
9 | | 2mwlk 26049 |
. . . . . . . . 9
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
10 | 8, 9 | syl6 34 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉))) |
11 | 10 | imp 444 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝐹(𝑉 Trails 𝐸)𝑃) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
12 | | imain 5888 |
. . . . . . . . . . 11
⊢ (Fun
◡𝑃 → (𝑃 “ ({0, (#‘𝐹)} ∩ (1..^(#‘𝐹)))) = ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹))))) |
13 | 12 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝑃) → (𝑃 “ ({0, (#‘𝐹)} ∩ (1..^(#‘𝐹)))) = ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹))))) |
14 | | 0lt1 10429 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
1 |
15 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ |
16 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ |
17 | 15, 16 | ltnlei 10037 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 < 1
↔ ¬ 1 ≤ 0) |
18 | 14, 17 | mpbi 219 |
. . . . . . . . . . . . . . . . 17
⊢ ¬ 1
≤ 0 |
19 | | elfzole1 12347 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
(1..^(#‘𝐹)) → 1
≤ 0) |
20 | 18, 19 | mto 187 |
. . . . . . . . . . . . . . . 16
⊢ ¬ 0
∈ (1..^(#‘𝐹)) |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Word dom 𝐸 → ¬ 0 ∈
(1..^(#‘𝐹))) |
22 | | wrdfin 13178 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹 ∈ Fin) |
23 | | hashcl 13009 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ Fin →
(#‘𝐹) ∈
ℕ0) |
24 | 23 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ Fin →
(#‘𝐹) ∈
ℝ) |
25 | 22, 24 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ Word dom 𝐸 → (#‘𝐹) ∈
ℝ) |
26 | 25 | ltnrd 10050 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Word dom 𝐸 → ¬ (#‘𝐹) < (#‘𝐹)) |
27 | 26 | intn3an3d 1436 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Word dom 𝐸 → ¬ ((#‘𝐹) ∈
(ℤ≥‘1) ∧ (#‘𝐹) ∈ ℤ ∧ (#‘𝐹) < (#‘𝐹))) |
28 | | elfzo2 12342 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) ∈
(1..^(#‘𝐹)) ↔
((#‘𝐹) ∈
(ℤ≥‘1) ∧ (#‘𝐹) ∈ ℤ ∧ (#‘𝐹) < (#‘𝐹))) |
29 | 27, 28 | sylnibr 318 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Word dom 𝐸 → ¬ (#‘𝐹) ∈ (1..^(#‘𝐹))) |
30 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(#‘𝐹) ∈
V |
31 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → (𝑥 ∈ (1..^(#‘𝐹)) ↔ 0 ∈ (1..^(#‘𝐹)))) |
32 | 31 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (¬ 𝑥 ∈ (1..^(#‘𝐹)) ↔ ¬ 0 ∈
(1..^(#‘𝐹)))) |
33 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (#‘𝐹) → (𝑥 ∈ (1..^(#‘𝐹)) ↔ (#‘𝐹) ∈ (1..^(#‘𝐹)))) |
34 | 33 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (#‘𝐹) → (¬ 𝑥 ∈ (1..^(#‘𝐹)) ↔ ¬ (#‘𝐹) ∈ (1..^(#‘𝐹)))) |
35 | 32, 34 | ralprg 4181 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ (#‘𝐹) ∈ V) → (∀𝑥 ∈ {0, (#‘𝐹)} ¬ 𝑥 ∈ (1..^(#‘𝐹)) ↔ (¬ 0 ∈
(1..^(#‘𝐹)) ∧
¬ (#‘𝐹) ∈
(1..^(#‘𝐹))))) |
36 | 15, 30, 35 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
{0, (#‘𝐹)} ¬
𝑥 ∈
(1..^(#‘𝐹)) ↔
(¬ 0 ∈ (1..^(#‘𝐹)) ∧ ¬ (#‘𝐹) ∈ (1..^(#‘𝐹)))) |
37 | 21, 29, 36 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word dom 𝐸 → ∀𝑥 ∈ {0, (#‘𝐹)} ¬ 𝑥 ∈ (1..^(#‘𝐹))) |
38 | | disj 3969 |
. . . . . . . . . . . . . 14
⊢ (({0,
(#‘𝐹)} ∩
(1..^(#‘𝐹))) =
∅ ↔ ∀𝑥
∈ {0, (#‘𝐹)}
¬ 𝑥 ∈
(1..^(#‘𝐹))) |
39 | 37, 38 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ Word dom 𝐸 → ({0, (#‘𝐹)} ∩ (1..^(#‘𝐹))) = ∅) |
40 | 39 | imaeq2d 5385 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ Word dom 𝐸 → (𝑃 “ ({0, (#‘𝐹)} ∩ (1..^(#‘𝐹)))) = (𝑃 “ ∅)) |
41 | | ima0 5400 |
. . . . . . . . . . . 12
⊢ (𝑃 “ ∅) =
∅ |
42 | 40, 41 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Word dom 𝐸 → (𝑃 “ ({0, (#‘𝐹)} ∩ (1..^(#‘𝐹)))) = ∅) |
43 | 42 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝑃) → (𝑃 “ ({0, (#‘𝐹)} ∩ (1..^(#‘𝐹)))) = ∅) |
44 | 13, 43 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝑃) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
45 | 44 | ex 449 |
. . . . . . . 8
⊢ (𝐹 ∈ Word dom 𝐸 → (Fun ◡𝑃 → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅)) |
46 | 45 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (Fun ◡𝑃 → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅)) |
47 | 11, 46 | syl 17 |
. . . . . 6
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝐹(𝑉 Trails 𝐸)𝑃) → (Fun ◡𝑃 → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅)) |
48 | 47 | impr 647 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
49 | 3, 6, 48 | 3jca 1235 |
. . . 4
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)) → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅)) |
50 | 49 | ex 449 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃) → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
51 | | isspth 26099 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
52 | | ispth 26098 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Paths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
53 | 50, 51, 52 | 3imtr4d 282 |
. 2
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 SPaths 𝐸)𝑃 → 𝐹(𝑉 Paths 𝐸)𝑃)) |
54 | 2, 53 | mpcom 37 |
1
⊢ (𝐹(𝑉 SPaths 𝐸)𝑃 → 𝐹(𝑉 Paths 𝐸)𝑃) |