Step | Hyp | Ref
| Expression |
1 | | mvrsval.w |
. . 3
β’ π = (mVarsβπ) |
2 | | elfvex 6881 |
. . . . 5
β’ (π β (mExβπ) β π β V) |
3 | | mvrsval.e |
. . . . 5
β’ πΈ = (mExβπ) |
4 | 2, 3 | eleq2s 2852 |
. . . 4
β’ (π β πΈ β π β V) |
5 | | fveq2 6843 |
. . . . . . 7
β’ (π‘ = π β (mExβπ‘) = (mExβπ)) |
6 | 5, 3 | eqtr4di 2791 |
. . . . . 6
β’ (π‘ = π β (mExβπ‘) = πΈ) |
7 | | fveq2 6843 |
. . . . . . . 8
β’ (π‘ = π β (mVRβπ‘) = (mVRβπ)) |
8 | | mvrsval.v |
. . . . . . . 8
β’ π = (mVRβπ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . 7
β’ (π‘ = π β (mVRβπ‘) = π) |
10 | 9 | ineq2d 4173 |
. . . . . 6
β’ (π‘ = π β (ran (2nd βπ) β© (mVRβπ‘)) = (ran (2nd
βπ) β© π)) |
11 | 6, 10 | mpteq12dv 5197 |
. . . . 5
β’ (π‘ = π β (π β (mExβπ‘) β¦ (ran (2nd βπ) β© (mVRβπ‘))) = (π β πΈ β¦ (ran (2nd βπ) β© π))) |
12 | | df-mvrs 34140 |
. . . . 5
β’ mVars =
(π‘ β V β¦ (π β (mExβπ‘) β¦ (ran (2nd
βπ) β©
(mVRβπ‘)))) |
13 | 11, 12, 3 | mptfvmpt 7179 |
. . . 4
β’ (π β V β
(mVarsβπ) = (π β πΈ β¦ (ran (2nd βπ) β© π))) |
14 | 4, 13 | syl 17 |
. . 3
β’ (π β πΈ β (mVarsβπ) = (π β πΈ β¦ (ran (2nd βπ) β© π))) |
15 | 1, 14 | eqtrid 2785 |
. 2
β’ (π β πΈ β π = (π β πΈ β¦ (ran (2nd βπ) β© π))) |
16 | | fveq2 6843 |
. . . . 5
β’ (π = π β (2nd βπ) = (2nd βπ)) |
17 | 16 | rneqd 5894 |
. . . 4
β’ (π = π β ran (2nd βπ) = ran (2nd
βπ)) |
18 | 17 | ineq1d 4172 |
. . 3
β’ (π = π β (ran (2nd βπ) β© π) = (ran (2nd βπ) β© π)) |
19 | 18 | adantl 483 |
. 2
β’ ((π β πΈ β§ π = π) β (ran (2nd βπ) β© π) = (ran (2nd βπ) β© π)) |
20 | | id 22 |
. 2
β’ (π β πΈ β π β πΈ) |
21 | | fvex 6856 |
. . . . 5
β’
(2nd βπ) β V |
22 | 21 | rnex 7850 |
. . . 4
β’ ran
(2nd βπ)
β V |
23 | 22 | inex1 5275 |
. . 3
β’ (ran
(2nd βπ)
β© π) β
V |
24 | 23 | a1i 11 |
. 2
β’ (π β πΈ β (ran (2nd βπ) β© π) β V) |
25 | 15, 19, 20, 24 | fvmptd 6956 |
1
β’ (π β πΈ β (πβπ) = (ran (2nd βπ) β© π)) |