Step | Hyp | Ref
| Expression |
1 | | df-br 4584 |
. . 3
⊢ (𝐹(𝑉 Paths 𝐸)𝑃 ↔ 〈𝐹, 𝑃〉 ∈ (𝑉 Paths 𝐸)) |
2 | | pths 26096 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 Paths 𝐸) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅)}) |
3 | 2 | adantr 480 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝑉 Paths 𝐸) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅)}) |
4 | 3 | eleq2d 2673 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (〈𝐹, 𝑃〉 ∈ (𝑉 Paths 𝐸) ↔ 〈𝐹, 𝑃〉 ∈ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅)})) |
5 | 1, 4 | syl5bb 271 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 Paths 𝐸)𝑃 ↔ 〈𝐹, 𝑃〉 ∈ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅)})) |
6 | | breq12 4588 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑓(𝑉 Trails 𝐸)𝑝 ↔ 𝐹(𝑉 Trails 𝐸)𝑃)) |
7 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃) |
8 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (#‘𝑓) = (#‘𝐹)) |
9 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (#‘𝑓) = (#‘𝐹)) |
10 | 9 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (1..^(#‘𝑓)) = (1..^(#‘𝐹))) |
11 | 7, 10 | reseq12d 5318 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑝 ↾ (1..^(#‘𝑓))) = (𝑃 ↾ (1..^(#‘𝐹)))) |
12 | 11 | cnveqd 5220 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ◡(𝑝 ↾ (1..^(#‘𝑓))) = ◡(𝑃 ↾ (1..^(#‘𝐹)))) |
13 | 12 | funeqd 5825 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ↔ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))) |
14 | 8 | preq2d 4219 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → {0, (#‘𝑓)} = {0, (#‘𝐹)}) |
15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → {0, (#‘𝑓)} = {0, (#‘𝐹)}) |
16 | 7, 15 | imaeq12d 5386 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑝 “ {0, (#‘𝑓)}) = (𝑃 “ {0, (#‘𝐹)})) |
17 | 8 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (1..^(#‘𝑓)) = (1..^(#‘𝐹))) |
18 | 17 | adantr 480 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (1..^(#‘𝑓)) = (1..^(#‘𝐹))) |
19 | 7, 18 | imaeq12d 5386 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑝 “ (1..^(#‘𝑓))) = (𝑃 “ (1..^(#‘𝐹)))) |
20 | 16, 19 | ineq12d 3777 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹))))) |
21 | 20 | eqeq1d 2612 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅ ↔ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅)) |
22 | 6, 13, 21 | 3anbi123d 1391 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ((𝑓(𝑉 Trails 𝐸)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅) ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
23 | 22 | opelopabga 4913 |
. . 3
⊢ ((𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍) → (〈𝐹, 𝑃〉 ∈ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅)} ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
24 | 23 | adantl 481 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (〈𝐹, 𝑃〉 ∈ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅)} ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
25 | 5, 24 | bitrd 267 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 Paths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |