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
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)}) ∈ V) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)}) ∈ V) |
11 | | simpl 472 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 𝑣 = 𝑉) |
12 | | oveq12 6558 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣 WalkOn 𝑒) = (𝑉 WalkOn 𝐸)) |
13 | 12 | oveqd 6566 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎(𝑣 WalkOn 𝑒)𝑏) = (𝑎(𝑉 WalkOn 𝐸)𝑏)) |
14 | 13 | breqd 4594 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ↔ 𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝)) |
15 | | oveq12 6558 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣 Trails 𝑒) = (𝑉 Trails 𝐸)) |
16 | 15 | breqd 4594 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑓(𝑣 Trails 𝑒)𝑝 ↔ 𝑓(𝑉 Trails 𝐸)𝑝)) |
17 | 14, 16 | anbi12d 743 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 Trails 𝑒)𝑝) ↔ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝))) |
18 | 17 | opabbidv 4648 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 Trails 𝑒)𝑝)} = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)}) |
19 | 11, 11, 18 | mpt2eq123dv 6615 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 Trails 𝑒)𝑝)}) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)})) |
20 | | df-trlon 26043 |
. . . . 5
⊢ TrailOn
= (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 Trails 𝑒)𝑝)})) |
21 | 19, 20 | ovmpt2ga 6688 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)}) ∈ V) → (𝑉 TrailOn 𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)})) |
22 | 2, 5, 10, 21 | syl3anc 1318 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑉 TrailOn 𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)})) |
23 | 22 | oveqd 6566 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 TrailOn 𝐸)𝐵) = (𝐴(𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)})𝐵)) |
24 | | simpl 472 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝑉) |
25 | 24 | adantl 481 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
26 | | simprr 792 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝐵 ∈ 𝑉) |
27 | | ancom 465 |
. . . . . . 7
⊢ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝) ↔ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝)) |
28 | 27 | a1i 11 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝) ↔ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝))) |
29 | 28 | opabbidv 4648 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)} = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝)}) |
30 | | trliswlk 26069 |
. . . . . . 7
⊢ (𝑓(𝑉 Trails 𝐸)𝑝 → 𝑓(𝑉 Walks 𝐸)𝑝) |
31 | 30 | wlkres 26050 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝)} ∈ V) |
32 | 1, 3, 31 | syl2an 493 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝)} ∈ V) |
33 | 29, 32 | eqeltrd 2688 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)} ∈ V) |
34 | 33 | adantr 480 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)} ∈ V) |
35 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎(𝑉 WalkOn 𝐸)𝑏) = (𝐴(𝑉 WalkOn 𝐸)𝐵)) |
36 | 35 | breqd 4594 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ↔ 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝)) |
37 | 36 | anbi1d 737 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝) ↔ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝))) |
38 | 37 | opabbidv 4648 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)} = {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)}) |
39 | | eqid 2610 |
. . . 4
⊢ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)}) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)}) |
40 | 38, 39 | ovmpt2ga 6688 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)} ∈ V) → (𝐴(𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)})𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)}) |
41 | 25, 26, 34, 40 | syl3anc 1318 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)})𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)}) |
42 | 23, 41 | eqtrd 2644 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 TrailOn 𝐸)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)}) |