Step | Hyp | Ref
| Expression |
1 | | otex 5426 |
. . . . 5
β’
β¨((1st β(1st βπ )) β© β¦βͺ ((mVarsβπ) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© β V |
2 | 1 | csbex 5272 |
. . . 4
β’
β¦(2nd βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© β V |
3 | 2 | csbex 5272 |
. . 3
β’
β¦(2nd β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© β V |
4 | | eqid 2733 |
. . . 4
β’
(mVarsβπ) =
(mVarsβπ) |
5 | | mpstssv.p |
. . . 4
β’ π = (mPreStβπ) |
6 | | msrf.r |
. . . 4
β’ π
= (mStRedβπ) |
7 | 4, 5, 6 | msrfval 34195 |
. . 3
β’ π
= (π β π β¦ β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) |
8 | 3, 7 | fnmpti 6648 |
. 2
β’ π
Fn π |
9 | 5 | mpst123 34198 |
. . . . . 6
β’ (π β π β π = β¨(1st
β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β©) |
10 | 9 | fveq2d 6850 |
. . . . 5
β’ (π β π β (π
βπ ) = (π
ββ¨(1st
β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β©)) |
11 | | id 22 |
. . . . . . 7
β’ (π β π β π β π) |
12 | 9, 11 | eqeltrrd 2835 |
. . . . . 6
β’ (π β π β β¨(1st
β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β© β
π) |
13 | | eqid 2733 |
. . . . . . 7
β’ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) = βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) |
14 | 4, 5, 6, 13 | msrval 34196 |
. . . . . 6
β’
(β¨(1st β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β© β
π β (π
ββ¨(1st
β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β©) =
β¨((1st β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) |
15 | 12, 14 | syl 17 |
. . . . 5
β’ (π β π β (π
ββ¨(1st
β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β©) =
β¨((1st β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) |
16 | 10, 15 | eqtrd 2773 |
. . . 4
β’ (π β π β (π
βπ ) = β¨((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) |
17 | | inss1 4192 |
. . . . . . 7
β’
((1st β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) β (1st
β(1st βπ )) |
18 | | eqid 2733 |
. . . . . . . . . . 11
β’
(mDVβπ) =
(mDVβπ) |
19 | | eqid 2733 |
. . . . . . . . . . 11
β’
(mExβπ) =
(mExβπ) |
20 | 18, 19, 5 | elmpst 34194 |
. . . . . . . . . 10
β’
(β¨(1st β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β© β
π β (((1st
β(1st βπ )) β (mDVβπ) β§ β‘(1st β(1st
βπ )) =
(1st β(1st βπ ))) β§ ((2nd
β(1st βπ )) β (mExβπ) β§ (2nd
β(1st βπ )) β Fin) β§ (2nd
βπ ) β
(mExβπ))) |
21 | 12, 20 | sylib 217 |
. . . . . . . . 9
β’ (π β π β (((1st
β(1st βπ )) β (mDVβπ) β§ β‘(1st β(1st
βπ )) =
(1st β(1st βπ ))) β§ ((2nd
β(1st βπ )) β (mExβπ) β§ (2nd
β(1st βπ )) β Fin) β§ (2nd
βπ ) β
(mExβπ))) |
22 | 21 | simp1d 1143 |
. . . . . . . 8
β’ (π β π β ((1st
β(1st βπ )) β (mDVβπ) β§ β‘(1st β(1st
βπ )) =
(1st β(1st βπ )))) |
23 | 22 | simpld 496 |
. . . . . . 7
β’ (π β π β (1st
β(1st βπ )) β (mDVβπ)) |
24 | 17, 23 | sstrid 3959 |
. . . . . 6
β’ (π β π β ((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) β (mDVβπ)) |
25 | | cnvin 6101 |
. . . . . . 7
β’ β‘((1st β(1st
βπ )) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) = (β‘(1st β(1st
βπ )) β© β‘(βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) |
26 | 22 | simprd 497 |
. . . . . . . 8
β’ (π β π β β‘(1st β(1st
βπ )) =
(1st β(1st βπ ))) |
27 | | cnvxp 6113 |
. . . . . . . . 9
β’ β‘(βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))) = (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))) |
28 | 27 | a1i 11 |
. . . . . . . 8
β’ (π β π β β‘(βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))) = (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) |
29 | 26, 28 | ineq12d 4177 |
. . . . . . 7
β’ (π β π β (β‘(1st β(1st
βπ )) β© β‘(βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) = ((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))))) |
30 | 25, 29 | eqtrid 2785 |
. . . . . 6
β’ (π β π β β‘((1st β(1st
βπ )) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) = ((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))))) |
31 | 24, 30 | jca 513 |
. . . . 5
β’ (π β π β (((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) β (mDVβπ) β§ β‘((1st β(1st
βπ )) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) = ((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))))) |
32 | 21 | simp2d 1144 |
. . . . 5
β’ (π β π β ((2nd
β(1st βπ )) β (mExβπ) β§ (2nd
β(1st βπ )) β Fin)) |
33 | 21 | simp3d 1145 |
. . . . 5
β’ (π β π β (2nd βπ ) β (mExβπ)) |
34 | 18, 19, 5 | elmpst 34194 |
. . . . 5
β’
(β¨((1st β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β© β π β ((((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) β (mDVβπ) β§ β‘((1st β(1st
βπ )) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) = ((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))))) β§ ((2nd
β(1st βπ )) β (mExβπ) β§ (2nd
β(1st βπ )) β Fin) β§ (2nd
βπ ) β
(mExβπ))) |
35 | 31, 32, 33, 34 | syl3anbrc 1344 |
. . . 4
β’ (π β π β β¨((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β© β π) |
36 | 16, 35 | eqeltrd 2834 |
. . 3
β’ (π β π β (π
βπ ) β π) |
37 | 36 | rgen 3063 |
. 2
β’
βπ β
π (π
βπ ) β π |
38 | | ffnfv 7070 |
. 2
β’ (π
:πβΆπ β (π
Fn π β§ βπ β π (π
βπ ) β π)) |
39 | 8, 37, 38 | mpbir2an 710 |
1
β’ π
:πβΆπ |