Theorem xkotf

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

	Ref	Expression
Hypotheses	xkoval.x	⊢ 𝑋 = ∪ 𝑅
	xkoval.k	⊢ 𝐾 = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp }
	xkoval.t	⊢ 𝑇 = ( 𝑘 ∈ 𝐾 , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
Assertion	xkotf	⊢ 𝑇 : ( 𝐾 × 𝑆 ) ⟶ 𝒫 ( 𝑅 Cn 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		xkoval.x	⊢ 𝑋 = ∪ 𝑅
2		xkoval.k	⊢ 𝐾 = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp }
3		xkoval.t	⊢ 𝑇 = ( 𝑘 ∈ 𝐾 , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
4		ovex	⊢ ( 𝑅 Cn 𝑆 ) ∈ V
5		ssrab2	⊢ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ⊆ ( 𝑅 Cn 𝑆 )
6	4 5	elpwi2	⊢ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ∈ 𝒫 ( 𝑅 Cn 𝑆 )
7	6	rgen2w	⊢ ∀ 𝑘 ∈ 𝐾 ∀ 𝑣 ∈ 𝑆 { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ∈ 𝒫 ( 𝑅 Cn 𝑆 )
8	3	fmpo	⊢ ( ∀ 𝑘 ∈ 𝐾 ∀ 𝑣 ∈ 𝑆 { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ∈ 𝒫 ( 𝑅 Cn 𝑆 ) ↔ 𝑇 : ( 𝐾 × 𝑆 ) ⟶ 𝒫 ( 𝑅 Cn 𝑆 ) )
9	7 8	mpbi	⊢ 𝑇 : ( 𝐾 × 𝑆 ) ⟶ 𝒫 ( 𝑅 Cn 𝑆 )