Step | Hyp | Ref
| Expression |
1 | | df-br 4584 |
. . 3
⊢ (𝐹(𝑉 Trails 𝐸)𝑃 ↔ 〈𝐹, 𝑃〉 ∈ (𝑉 Trails 𝐸)) |
2 | | trls 26066 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 Trails 𝐸) = {〈𝑓, 𝑝〉 ∣ ((𝑓 ∈ Word dom 𝐸 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
3 | 2 | adantr 480 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝑉 Trails 𝐸) = {〈𝑓, 𝑝〉 ∣ ((𝑓 ∈ Word dom 𝐸 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
4 | 3 | eleq2d 2673 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (〈𝐹, 𝑃〉 ∈ (𝑉 Trails 𝐸) ↔ 〈𝐹, 𝑃〉 ∈ {〈𝑓, 𝑝〉 ∣ ((𝑓 ∈ Word dom 𝐸 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})) |
5 | 1, 4 | syl5bb 271 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ 〈𝐹, 𝑃〉 ∈ {〈𝑓, 𝑝〉 ∣ ((𝑓 ∈ Word dom 𝐸 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})) |
6 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓 ∈ Word dom 𝐸 ↔ 𝐹 ∈ Word dom 𝐸)) |
7 | | cnveq 5218 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹) |
8 | 7 | funeqd 5825 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (Fun ◡𝑓 ↔ Fun ◡𝐹)) |
9 | 6, 8 | anbi12d 743 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑓 ∈ Word dom 𝐸 ∧ Fun ◡𝑓) ↔ (𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹))) |
10 | 9 | adantr 480 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ((𝑓 ∈ Word dom 𝐸 ∧ Fun ◡𝑓) ↔ (𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹))) |
11 | | simpr 476 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃) |
12 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (#‘𝑓) = (#‘𝐹)) |
13 | 12 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (0...(#‘𝑓)) = (0...(#‘𝐹))) |
14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (0...(#‘𝑓)) = (0...(#‘𝐹))) |
15 | 11, 14 | feq12d 5946 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑝:(0...(#‘𝑓))⟶𝑉 ↔ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
16 | 12 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (0..^(#‘𝑓)) = (0..^(#‘𝐹))) |
17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (0..^(#‘𝑓)) = (0..^(#‘𝐹))) |
18 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓‘𝑘) = (𝐹‘𝑘)) |
19 | 18 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝐸‘(𝑓‘𝑘)) = (𝐸‘(𝐹‘𝑘))) |
20 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (𝑝‘𝑘) = (𝑃‘𝑘)) |
21 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (𝑝‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))) |
22 | 20, 21 | preq12d 4220 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
23 | 19, 22 | eqeqan12d 2626 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ((𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
24 | 17, 23 | raleqbidv 3129 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
25 | 10, 15, 24 | 3anbi123d 1391 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (((𝑓 ∈ Word dom 𝐸 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
26 | 25 | opelopabga 4913 |
. . 3
⊢ ((𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍) → (〈𝐹, 𝑃〉 ∈ {〈𝑓, 𝑝〉 ∣ ((𝑓 ∈ Word dom 𝐸 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
27 | 26 | adantl 481 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (〈𝐹, 𝑃〉 ∈ {〈𝑓, 𝑝〉 ∣ ((𝑓 ∈ Word dom 𝐸 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
28 | 5, 27 | bitrd 267 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |