Theorem xkotf

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

	Ref	Expression
Hypotheses	xkoval.x	$$⊢X=\bigcup R$$
	xkoval.k	$$⊢K=\left\{x\in 𝒫X|R{\upharpoonright }_{𝑡}x\in \mathrm{Comp}\right\}$$
	xkoval.t	$$⊢T=\left(k\in K,v\in S⟼\left\{f\in \left(R\mathrm{Cn}S\right)|f\left[k\right]\subseteq v\right\}\right)$$
Assertion	xkotf	$$⊢T:K\times S⟶𝒫\left(R\mathrm{Cn}S\right)$$

Proof

Step	Hyp	Ref	Expression
1		xkoval.x	$$⊢X=\bigcup R$$
2		xkoval.k	$$⊢K=\left\{x\in 𝒫X|R{\upharpoonright }_{𝑡}x\in \mathrm{Comp}\right\}$$
3		xkoval.t	$$⊢T=\left(k\in K,v\in S⟼\left\{f\in \left(R\mathrm{Cn}S\right)|f\left[k\right]\subseteq v\right\}\right)$$
4		ovex	$$⊢R\mathrm{Cn}S\in \mathrm{V}$$
5		ssrab2	$$⊢\left\{f\in \left(R\mathrm{Cn}S\right)|f\left[k\right]\subseteq v\right\}\subseteq R\mathrm{Cn}S$$
6	4 5	elpwi2	$$⊢\left\{f\in \left(R\mathrm{Cn}S\right)|f\left[k\right]\subseteq v\right\}\in 𝒫\left(R\mathrm{Cn}S\right)$$
7	6	rgen2w	$$⊢\forall k\in K\forall v\in S\left\{f\in \left(R\mathrm{Cn}S\right)|f\left[k\right]\subseteq v\right\}\in 𝒫\left(R\mathrm{Cn}S\right)$$
8	3	fmpo	$$⊢\forall k\in K\forall v\in S\left\{f\in \left(R\mathrm{Cn}S\right)|f\left[k\right]\subseteq v\right\}\in 𝒫\left(R\mathrm{Cn}S\right)\leftrightarrow T:K\times S⟶𝒫\left(R\mathrm{Cn}S\right)$$
9	7 8	mpbi	$$⊢T:K\times S⟶𝒫\left(R\mathrm{Cn}S\right)$$