Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’
(mVRβπ) =
(mVRβπ) |
2 | | eqid 2733 |
. . . . . 6
β’
(mRExβπ) =
(mRExβπ) |
3 | | elmsubrn.s |
. . . . . 6
β’ π = (mSubstβπ) |
4 | | elmsubrn.e |
. . . . . 6
β’ πΈ = (mExβπ) |
5 | | elmsubrn.o |
. . . . . 6
β’ π = (mRSubstβπ) |
6 | 1, 2, 3, 4, 5 | msubffval 34181 |
. . . . 5
β’ (π β V β π = (π β ((mRExβπ) βpm (mVRβπ)) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©))) |
7 | 1, 2, 5 | mrsubff 34170 |
. . . . . . . 8
β’ (π β V β π:((mRExβπ) βpm (mVRβπ))βΆ((mRExβπ) βm
(mRExβπ))) |
8 | 7 | ffnd 6673 |
. . . . . . 7
β’ (π β V β π Fn ((mRExβπ) βpm
(mVRβπ))) |
9 | | fnfvelrn 7035 |
. . . . . . 7
β’ ((π Fn ((mRExβπ) βpm
(mVRβπ)) β§ π β ((mRExβπ) βpm
(mVRβπ))) β
(πβπ) β ran π) |
10 | 8, 9 | sylan 581 |
. . . . . 6
β’ ((π β V β§ π β ((mRExβπ) βpm
(mVRβπ))) β
(πβπ) β ran π) |
11 | 7 | feqmptd 6914 |
. . . . . 6
β’ (π β V β π = (π β ((mRExβπ) βpm (mVRβπ)) β¦ (πβπ))) |
12 | | eqidd 2734 |
. . . . . 6
β’ (π β V β (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) = (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©))) |
13 | | fveq1 6845 |
. . . . . . . 8
β’ (π = (πβπ) β (πβ(2nd βπ)) = ((πβπ)β(2nd βπ))) |
14 | 13 | opeq2d 4841 |
. . . . . . 7
β’ (π = (πβπ) β β¨(1st βπ), (πβ(2nd βπ))β© = β¨(1st
βπ), ((πβπ)β(2nd βπ))β©) |
15 | 14 | mpteq2dv 5211 |
. . . . . 6
β’ (π = (πβπ) β (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) = (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©)) |
16 | 10, 11, 12, 15 | fmptco 7079 |
. . . . 5
β’ (π β V β ((π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) β π) = (π β ((mRExβπ) βpm (mVRβπ)) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©))) |
17 | 6, 16 | eqtr4d 2776 |
. . . 4
β’ (π β V β π = ((π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) β π)) |
18 | 17 | rneqd 5897 |
. . 3
β’ (π β V β ran π = ran ((π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) β π)) |
19 | | rnco 6208 |
. . . 4
β’ ran
((π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) β π) = ran ((π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) βΎ ran π) |
20 | | ssid 3970 |
. . . . . 6
β’ ran π β ran π |
21 | | resmpt 5995 |
. . . . . 6
β’ (ran
π β ran π β ((π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) βΎ ran π) = (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©))) |
22 | 20, 21 | ax-mp 5 |
. . . . 5
β’ ((π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) βΎ ran π) = (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) |
23 | 22 | rneqi 5896 |
. . . 4
β’ ran
((π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) βΎ ran π) = ran (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) |
24 | 19, 23 | eqtri 2761 |
. . 3
β’ ran
((π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) β π) = ran (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) |
25 | 18, 24 | eqtrdi 2789 |
. 2
β’ (π β V β ran π = ran (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©))) |
26 | | mpt0 6647 |
. . . . 5
β’ (π β β
β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) =
β
|
27 | 26 | eqcomi 2742 |
. . . 4
β’ β
=
(π β β
β¦
(π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) |
28 | | fvprc 6838 |
. . . . 5
β’ (Β¬
π β V β
(mSubstβπ) =
β
) |
29 | 3, 28 | eqtrid 2785 |
. . . 4
β’ (Β¬
π β V β π = β
) |
30 | 5 | rnfvprc 6840 |
. . . . 5
β’ (Β¬
π β V β ran π = β
) |
31 | 30 | mpteq1d 5204 |
. . . 4
β’ (Β¬
π β V β (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) = (π β β
β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©))) |
32 | 27, 29, 31 | 3eqtr4a 2799 |
. . 3
β’ (Β¬
π β V β π = (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©))) |
33 | 32 | rneqd 5897 |
. 2
β’ (Β¬
π β V β ran π = ran (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©))) |
34 | 25, 33 | pm2.61i 182 |
1
β’ ran π = ran (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) |