Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. . . . 5
⊢ (𝑉 ∈ 𝑋 → 𝑉 ∈ V) |
2 | 1 | ad2antrr 758 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝑉 ∈ V) |
3 | | elex 3185 |
. . . . . 6
⊢ (𝐸 ∈ 𝑌 → 𝐸 ∈ V) |
4 | 3 | adantl 481 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ∈ V) |
5 | 4 | adantr 480 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝐸 ∈ V) |
6 | | id 22 |
. . . . . . 7
⊢ (𝑉 ∈ 𝑋 → 𝑉 ∈ 𝑋) |
7 | 6 | ancli 572 |
. . . . . 6
⊢ (𝑉 ∈ 𝑋 → (𝑉 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋)) |
8 | 7 | ad2antrr 758 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑉 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋)) |
9 | | mpt2exga 7135 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}) ∈ V) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}) ∈ V) |
11 | | simpl 472 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 𝑣 = 𝑉) |
12 | | oveq12 6558 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣 Walks 𝑒) = (𝑉 Walks 𝐸)) |
13 | 12 | breqd 4594 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑓(𝑣 Walks 𝑒)𝑝 ↔ 𝑓(𝑉 Walks 𝐸)𝑝)) |
14 | 13 | 3anbi1d 1395 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏) ↔ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏))) |
15 | 14 | opabbidv 4648 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)} = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}) |
16 | 11, 11, 15 | mpt2eq123dv 6615 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})) |
17 | | df-wlkon 26042 |
. . . . 5
⊢ WalkOn =
(𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})) |
18 | 16, 17 | ovmpt2ga 6688 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}) ∈ V) → (𝑉 WalkOn 𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})) |
19 | 2, 5, 10, 18 | syl3anc 1318 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑉 WalkOn 𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})) |
20 | 19 | oveqd 6566 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 WalkOn 𝐸)𝐵) = (𝐴(𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})𝐵)) |
21 | | simpl 472 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝑉) |
22 | 21 | adantl 481 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
23 | | simprr 792 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝐵 ∈ 𝑉) |
24 | | 3anass 1035 |
. . . . . . 7
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵) ↔ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵))) |
25 | 24 | a1i 11 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵) ↔ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵)))) |
26 | 25 | opabbidv 4648 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵)} = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵))}) |
27 | | id 22 |
. . . . . . 7
⊢ (𝑓(𝑉 Walks 𝐸)𝑝 → 𝑓(𝑉 Walks 𝐸)𝑝) |
28 | 27 | wlkres 26050 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵))} ∈ V) |
29 | 1, 3, 28 | syl2an 493 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵))} ∈ V) |
30 | 26, 29 | eqeltrd 2688 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵)} ∈ V) |
31 | 30 | adantr 480 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵)} ∈ V) |
32 | | eqeq2 2621 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝑝‘0) = 𝑎 ↔ (𝑝‘0) = 𝐴)) |
33 | 32 | adantr 480 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑝‘0) = 𝑎 ↔ (𝑝‘0) = 𝐴)) |
34 | | eqeq2 2621 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → ((𝑝‘(#‘𝑓)) = 𝑏 ↔ (𝑝‘(#‘𝑓)) = 𝐵)) |
35 | 34 | adantl 481 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑝‘(#‘𝑓)) = 𝑏 ↔ (𝑝‘(#‘𝑓)) = 𝐵)) |
36 | 33, 35 | 3anbi23d 1394 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏) ↔ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵))) |
37 | 36 | opabbidv 4648 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)} = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵)}) |
38 | | eqid 2610 |
. . . 4
⊢ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}) |
39 | 37, 38 | ovmpt2ga 6688 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵)} ∈ V) → (𝐴(𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵)}) |
40 | 22, 23, 31, 39 | syl3anc 1318 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵)}) |
41 | 20, 40 | eqtrd 2644 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 WalkOn 𝐸)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵)}) |