Step | Hyp | Ref
| Expression |
1 | | xp1st 7957 |
. . . . . . . . 9
β’ (π β ((mTCβπ) Γ π
) β (1st βπ) β (mTCβπ)) |
2 | | eqid 2733 |
. . . . . . . . . 10
β’
(mTCβπ) =
(mTCβπ) |
3 | | msubff.e |
. . . . . . . . . 10
β’ πΈ = (mExβπ) |
4 | | msubff.r |
. . . . . . . . . 10
β’ π
= (mRExβπ) |
5 | 2, 3, 4 | mexval 34160 |
. . . . . . . . 9
β’ πΈ = ((mTCβπ) Γ π
) |
6 | 1, 5 | eleq2s 2852 |
. . . . . . . 8
β’ (π β πΈ β (1st βπ) β (mTCβπ)) |
7 | 6 | adantl 483 |
. . . . . . 7
β’ (((π β π β§ π β (π
βpm π)) β§ π β πΈ) β (1st βπ) β (mTCβπ)) |
8 | | msubff.v |
. . . . . . . . . . 11
β’ π = (mVRβπ) |
9 | | eqid 2733 |
. . . . . . . . . . 11
β’
(mRSubstβπ) =
(mRSubstβπ) |
10 | 8, 4, 9 | mrsubff 34170 |
. . . . . . . . . 10
β’ (π β π β (mRSubstβπ):(π
βpm π)βΆ(π
βm π
)) |
11 | 10 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((π β π β§ π β (π
βpm π)) β ((mRSubstβπ)βπ) β (π
βm π
)) |
12 | | elmapi 8793 |
. . . . . . . . 9
β’
(((mRSubstβπ)βπ) β (π
βm π
) β ((mRSubstβπ)βπ):π
βΆπ
) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
β’ ((π β π β§ π β (π
βpm π)) β ((mRSubstβπ)βπ):π
βΆπ
) |
14 | | xp2nd 7958 |
. . . . . . . . 9
β’ (π β ((mTCβπ) Γ π
) β (2nd βπ) β π
) |
15 | 14, 5 | eleq2s 2852 |
. . . . . . . 8
β’ (π β πΈ β (2nd βπ) β π
) |
16 | | ffvelcdm 7036 |
. . . . . . . 8
β’
((((mRSubstβπ)βπ):π
βΆπ
β§ (2nd βπ) β π
) β (((mRSubstβπ)βπ)β(2nd βπ)) β π
) |
17 | 13, 15, 16 | syl2an 597 |
. . . . . . 7
β’ (((π β π β§ π β (π
βpm π)) β§ π β πΈ) β (((mRSubstβπ)βπ)β(2nd βπ)) β π
) |
18 | | opelxp 5673 |
. . . . . . 7
β’
(β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β© β
((mTCβπ) Γ
π
) β ((1st
βπ) β
(mTCβπ) β§
(((mRSubstβπ)βπ)β(2nd βπ)) β π
)) |
19 | 7, 17, 18 | sylanbrc 584 |
. . . . . 6
β’ (((π β π β§ π β (π
βpm π)) β§ π β πΈ) β β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β© β
((mTCβπ) Γ
π
)) |
20 | 19, 5 | eleqtrrdi 2845 |
. . . . 5
β’ (((π β π β§ π β (π
βpm π)) β§ π β πΈ) β β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β© β πΈ) |
21 | 20 | fmpttd 7067 |
. . . 4
β’ ((π β π β§ π β (π
βpm π)) β (π β πΈ β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©):πΈβΆπΈ) |
22 | 3 | fvexi 6860 |
. . . . 5
β’ πΈ β V |
23 | 22, 22 | elmap 8815 |
. . . 4
β’ ((π β πΈ β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©) β (πΈ βm πΈ) β (π β πΈ β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©):πΈβΆπΈ) |
24 | 21, 23 | sylibr 233 |
. . 3
β’ ((π β π β§ π β (π
βpm π)) β (π β πΈ β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©) β (πΈ βm πΈ)) |
25 | 24 | fmpttd 7067 |
. 2
β’ (π β π β (π β (π
βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©)):(π
βpm π)βΆ(πΈ βm πΈ)) |
26 | | msubff.s |
. . . 4
β’ π = (mSubstβπ) |
27 | 8, 4, 26, 3, 9 | msubffval 34181 |
. . 3
β’ (π β π β π = (π β (π
βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©))) |
28 | 27 | feq1d 6657 |
. 2
β’ (π β π β (π:(π
βpm π)βΆ(πΈ βm πΈ) β (π β (π
βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©)):(π
βpm π)βΆ(πΈ βm πΈ))) |
29 | 25, 28 | mpbird 257 |
1
β’ (π β π β π:(π
βpm π)βΆ(πΈ βm πΈ)) |