Step | Hyp | Ref
| Expression |
1 | | msrfval.r |
. 2
β’ π
= (mStRedβπ) |
2 | | fveq2 6846 |
. . . . . 6
β’ (π‘ = π β (mPreStβπ‘) = (mPreStβπ)) |
3 | | msrfval.p |
. . . . . 6
β’ π = (mPreStβπ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . 5
β’ (π‘ = π β (mPreStβπ‘) = π) |
5 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (mVarsβπ‘) = (mVarsβπ)) |
6 | | msrfval.v |
. . . . . . . . . . . . 13
β’ π = (mVarsβπ) |
7 | 5, 6 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ (π‘ = π β (mVarsβπ‘) = π) |
8 | 7 | imaeq1d 6016 |
. . . . . . . . . . 11
β’ (π‘ = π β ((mVarsβπ‘) β (β βͺ {π})) = (π β (β βͺ {π}))) |
9 | 8 | unieqd 4883 |
. . . . . . . . . 10
β’ (π‘ = π β βͺ
((mVarsβπ‘) β
(β βͺ {π})) = βͺ (π β (β βͺ {π}))) |
10 | 9 | csbeq1d 3863 |
. . . . . . . . 9
β’ (π‘ = π β β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§) = β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)) |
11 | 10 | ineq2d 4176 |
. . . . . . . 8
β’ (π‘ = π β ((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)) = ((1st β(1st
βπ )) β©
β¦βͺ (π β (β βͺ {π})) / π§β¦(π§ Γ π§))) |
12 | 11 | oteq1d 4846 |
. . . . . . 7
β’ (π‘ = π β β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© = β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) |
13 | 12 | csbeq2dv 3866 |
. . . . . 6
β’ (π‘ = π β β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© = β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) |
14 | 13 | csbeq2dv 3866 |
. . . . 5
β’ (π‘ = π β β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© = β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) |
15 | 4, 14 | mpteq12dv 5200 |
. . . 4
β’ (π‘ = π β (π β (mPreStβπ‘) β¦ β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) = (π β π β¦ β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©)) |
16 | | df-msr 34152 |
. . . 4
β’ mStRed =
(π‘ β V β¦ (π β (mPreStβπ‘) β¦
β¦(2nd β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©)) |
17 | 15, 16, 3 | mptfvmpt 7182 |
. . 3
β’ (π β V β
(mStRedβπ) = (π β π β¦ β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©)) |
18 | | mpt0 6647 |
. . . . 5
β’ (π β β
β¦
β¦(2nd β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) = β
|
19 | 18 | eqcomi 2742 |
. . . 4
β’ β
=
(π β β
β¦
β¦(2nd β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) |
20 | | fvprc 6838 |
. . . 4
β’ (Β¬
π β V β
(mStRedβπ) =
β
) |
21 | | fvprc 6838 |
. . . . . 6
β’ (Β¬
π β V β
(mPreStβπ) =
β
) |
22 | 3, 21 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π β V β π = β
) |
23 | 22 | mpteq1d 5204 |
. . . 4
β’ (Β¬
π β V β (π β π β¦ β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) = (π β β
β¦
β¦(2nd β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©)) |
24 | 19, 20, 23 | 3eqtr4a 2799 |
. . 3
β’ (Β¬
π β V β
(mStRedβπ) = (π β π β¦ β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©)) |
25 | 17, 24 | pm2.61i 182 |
. 2
β’
(mStRedβπ) =
(π β π β¦ β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) |
26 | 1, 25 | eqtri 2761 |
1
β’ π
= (π β π β¦ β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) |