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 ⊢ 𝑋 = ∪ 𝑅
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 𝑆 )