Step | Hyp | Ref
| Expression |
1 | | elex 3431 |
. 2
⊢ (𝑇 ∈ 𝑊 → 𝑇 ∈ V) |
2 | | msubffval.s |
. . 3
⊢ 𝑆 = (mSubst‘𝑇) |
3 | | fveq2 6722 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (mREx‘𝑡) = (mREx‘𝑇)) |
4 | | msubffval.r |
. . . . . . 7
⊢ 𝑅 = (mREx‘𝑇) |
5 | 3, 4 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (mREx‘𝑡) = 𝑅) |
6 | | fveq2 6722 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (mVR‘𝑡) = (mVR‘𝑇)) |
7 | | msubffval.v |
. . . . . . 7
⊢ 𝑉 = (mVR‘𝑇) |
8 | 6, 7 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (mVR‘𝑡) = 𝑉) |
9 | 5, 8 | oveq12d 7236 |
. . . . 5
⊢ (𝑡 = 𝑇 → ((mREx‘𝑡) ↑pm (mVR‘𝑡)) = (𝑅 ↑pm 𝑉)) |
10 | | fveq2 6722 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (mEx‘𝑡) = (mEx‘𝑇)) |
11 | | msubffval.e |
. . . . . . 7
⊢ 𝐸 = (mEx‘𝑇) |
12 | 10, 11 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (mEx‘𝑡) = 𝐸) |
13 | | fveq2 6722 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → (mRSubst‘𝑡) = (mRSubst‘𝑇)) |
14 | | msubffval.o |
. . . . . . . . . 10
⊢ 𝑂 = (mRSubst‘𝑇) |
15 | 13, 14 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (mRSubst‘𝑡) = 𝑂) |
16 | 15 | fveq1d 6724 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → ((mRSubst‘𝑡)‘𝑓) = (𝑂‘𝑓)) |
17 | 16 | fveq1d 6724 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒)) = ((𝑂‘𝑓)‘(2nd ‘𝑒))) |
18 | 17 | opeq2d 4796 |
. . . . . 6
⊢ (𝑡 = 𝑇 → 〈(1st ‘𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))〉 = 〈(1st
‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉) |
19 | 12, 18 | mpteq12dv 5145 |
. . . . 5
⊢ (𝑡 = 𝑇 → (𝑒 ∈ (mEx‘𝑡) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))〉) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉)) |
20 | 9, 19 | mpteq12dv 5145 |
. . . 4
⊢ (𝑡 = 𝑇 → (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))〉)) = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) |
21 | | df-msub 33171 |
. . . 4
⊢ mSubst =
(𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm
(mVR‘𝑡)) ↦
(𝑒 ∈ (mEx‘𝑡) ↦ 〈(1st
‘𝑒),
(((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))〉))) |
22 | | ovex 7251 |
. . . . 5
⊢ (𝑅 ↑pm 𝑉) ∈ V |
23 | 22 | mptex 7044 |
. . . 4
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉)) ∈
V |
24 | 20, 21, 23 | fvmpt 6823 |
. . 3
⊢ (𝑇 ∈ V →
(mSubst‘𝑇) = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) |
25 | 2, 24 | syl5eq 2790 |
. 2
⊢ (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) |
26 | 1, 25 | syl 17 |
1
⊢ (𝑇 ∈ 𝑊 → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) |