Step |
Hyp |
Ref |
Expression |
1 |
|
xkoval.x |
|- X = U. R |
2 |
|
xkoval.k |
|- K = { x e. ~P X | ( R |`t x ) e. Comp } |
3 |
|
xkoval.t |
|- T = ( k e. K , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) |
4 |
|
ovex |
|- ( R Cn S ) e. _V |
5 |
|
ssrab2 |
|- { f e. ( R Cn S ) | ( f " k ) C_ v } C_ ( R Cn S ) |
6 |
4 5
|
elpwi2 |
|- { f e. ( R Cn S ) | ( f " k ) C_ v } e. ~P ( R Cn S ) |
7 |
6
|
rgen2w |
|- A. k e. K A. v e. S { f e. ( R Cn S ) | ( f " k ) C_ v } e. ~P ( R Cn S ) |
8 |
3
|
fmpo |
|- ( A. k e. K A. v e. S { f e. ( R Cn S ) | ( f " k ) C_ v } e. ~P ( R Cn S ) <-> T : ( K X. S ) --> ~P ( R Cn S ) ) |
9 |
7 8
|
mpbi |
|- T : ( K X. S ) --> ~P ( R Cn S ) |