Step | Hyp | Ref
| Expression |
1 | | pthsfval 28958 |
. . . 4
⊢
(Paths‘𝐺) =
{〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) =
∅)} |
2 | | 3anass 1096 |
. . . . 5
⊢ ((𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅) ↔ (𝑓(Trails‘𝐺)𝑝 ∧ (Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) =
∅))) |
3 | 2 | opabbii 5214 |
. . . 4
⊢
{〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅)} = {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝐺)𝑝 ∧ (Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) =
∅))} |
4 | 1, 3 | eqtri 2761 |
. . 3
⊢
(Paths‘𝐺) =
{〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝐺)𝑝 ∧ (Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) =
∅))} |
5 | | simpr 486 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃) |
6 | | fveq2 6888 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (♯‘𝑓) = (♯‘𝐹)) |
7 | 6 | oveq2d 7420 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (1..^(♯‘𝑓)) = (1..^(♯‘𝐹))) |
8 | 7 | adantr 482 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (1..^(♯‘𝑓)) = (1..^(♯‘𝐹))) |
9 | 5, 8 | reseq12d 5980 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑝 ↾ (1..^(♯‘𝑓))) = (𝑃 ↾ (1..^(♯‘𝐹)))) |
10 | 9 | cnveqd 5873 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ◡(𝑝 ↾ (1..^(♯‘𝑓))) = ◡(𝑃 ↾ (1..^(♯‘𝐹)))) |
11 | 10 | funeqd 6567 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ↔ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))))) |
12 | 6 | preq2d 4743 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → {0, (♯‘𝑓)} = {0, (♯‘𝐹)}) |
13 | 12 | adantr 482 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → {0, (♯‘𝑓)} = {0, (♯‘𝐹)}) |
14 | 5, 13 | imaeq12d 6058 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑝 “ {0, (♯‘𝑓)}) = (𝑃 “ {0, (♯‘𝐹)})) |
15 | 5, 8 | imaeq12d 6058 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑝 “ (1..^(♯‘𝑓))) = (𝑃 “ (1..^(♯‘𝐹)))) |
16 | 14, 15 | ineq12d 4212 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹))))) |
17 | 16 | eqeq1d 2735 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅ ↔ ((𝑃 “ {0,
(♯‘𝐹)}) ∩
(𝑃 “
(1..^(♯‘𝐹)))) =
∅)) |
18 | 11, 17 | anbi12d 632 |
. . 3
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ((Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅) ↔ (Fun
◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) =
∅))) |
19 | | reltrls 28931 |
. . 3
⊢ Rel
(Trails‘𝐺) |
20 | 4, 18, 19 | brfvopabrbr 6991 |
. 2
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ (Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) =
∅))) |
21 | | 3anass 1096 |
. 2
⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅) ↔ (𝐹(Trails‘𝐺)𝑃 ∧ (Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) =
∅))) |
22 | 20, 21 | bitr4i 278 |
1
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) =
∅)) |