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 )