This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xkotf

Description: Functionality of function T . (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses xkoval.x 
|- X = U. R
xkoval.k 
|- K = { x e. ~P X | ( R |`t x ) e. Comp }
xkoval.t 
|- T = ( k e. K , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } )
Assertion xkotf 
|- T : ( K X. S ) --> ~P ( R Cn S )

Proof

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 )