Step | Hyp | Ref
| Expression |
1 | | mthmval.u |
. 2
β’ π = (mThmβπ) |
2 | | fveq2 6890 |
. . . . . . 7
β’ (π‘ = π β (mStRedβπ‘) = (mStRedβπ)) |
3 | | mthmval.r |
. . . . . . 7
β’ π
= (mStRedβπ) |
4 | 2, 3 | eqtr4di 2788 |
. . . . . 6
β’ (π‘ = π β (mStRedβπ‘) = π
) |
5 | 4 | cnveqd 5874 |
. . . . 5
β’ (π‘ = π β β‘(mStRedβπ‘) = β‘π
) |
6 | | fveq2 6890 |
. . . . . . 7
β’ (π‘ = π β (mPPStβπ‘) = (mPPStβπ)) |
7 | | mthmval.j |
. . . . . . 7
β’ π½ = (mPPStβπ) |
8 | 6, 7 | eqtr4di 2788 |
. . . . . 6
β’ (π‘ = π β (mPPStβπ‘) = π½) |
9 | 4, 8 | imaeq12d 6059 |
. . . . 5
β’ (π‘ = π β ((mStRedβπ‘) β (mPPStβπ‘)) = (π
β π½)) |
10 | 5, 9 | imaeq12d 6059 |
. . . 4
β’ (π‘ = π β (β‘(mStRedβπ‘) β ((mStRedβπ‘) β (mPPStβπ‘))) = (β‘π
β (π
β π½))) |
11 | | df-mthm 34788 |
. . . 4
β’ mThm =
(π‘ β V β¦ (β‘(mStRedβπ‘) β ((mStRedβπ‘) β (mPPStβπ‘)))) |
12 | | fvex 6903 |
. . . . . 6
β’
(mStRedβπ‘)
β V |
13 | 12 | cnvex 7918 |
. . . . 5
β’ β‘(mStRedβπ‘) β V |
14 | | imaexg 7908 |
. . . . 5
β’ (β‘(mStRedβπ‘) β V β (β‘(mStRedβπ‘) β ((mStRedβπ‘) β (mPPStβπ‘))) β V) |
15 | 13, 14 | ax-mp 5 |
. . . 4
β’ (β‘(mStRedβπ‘) β ((mStRedβπ‘) β (mPPStβπ‘))) β V |
16 | 10, 11, 15 | fvmpt3i 7002 |
. . 3
β’ (π β V β
(mThmβπ) = (β‘π
β (π
β π½))) |
17 | | 0ima 6076 |
. . . . 5
β’ (β
β (π
β π½)) = β
|
18 | 17 | eqcomi 2739 |
. . . 4
β’ β
=
(β
β (π
β
π½)) |
19 | | fvprc 6882 |
. . . 4
β’ (Β¬
π β V β
(mThmβπ) =
β
) |
20 | | fvprc 6882 |
. . . . . . . 8
β’ (Β¬
π β V β
(mStRedβπ) =
β
) |
21 | 3, 20 | eqtrid 2782 |
. . . . . . 7
β’ (Β¬
π β V β π
= β
) |
22 | 21 | cnveqd 5874 |
. . . . . 6
β’ (Β¬
π β V β β‘π
= β‘β
) |
23 | | cnv0 6139 |
. . . . . 6
β’ β‘β
= β
|
24 | 22, 23 | eqtrdi 2786 |
. . . . 5
β’ (Β¬
π β V β β‘π
= β
) |
25 | 24 | imaeq1d 6057 |
. . . 4
β’ (Β¬
π β V β (β‘π
β (π
β π½)) = (β
β (π
β π½))) |
26 | 18, 19, 25 | 3eqtr4a 2796 |
. . 3
β’ (Β¬
π β V β
(mThmβπ) = (β‘π
β (π
β π½))) |
27 | 16, 26 | pm2.61i 182 |
. 2
β’
(mThmβπ) =
(β‘π
β (π
β π½)) |
28 | 1, 27 | eqtri 2758 |
1
β’ π = (β‘π
β (π
β π½)) |