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 = ⋃ R
xkoval.k ⊢ K = x ∈ 𝒫 X | R ↾ 𝑡 x ∈ Comp
xkoval.t ⊢ T = k ∈ K , v ∈ S ⟼ f ∈ R Cn S | f k ⊆ v
Assertion xkotf ⊢ T : K × S ⟶ 𝒫 R Cn S

Proof

Step Hyp Ref Expression
1 xkoval.x ⊢ X = ⋃ R
2 xkoval.k ⊢ K = x ∈ 𝒫 X | R ↾ 𝑡 x ∈ Comp
3 xkoval.t ⊢ T = k ∈ K , v ∈ S ⟼ f ∈ R Cn S | f k ⊆ v
4 ovex ⊢ R Cn S ∈ V
5 ssrab2 ⊢ f ∈ R Cn S | f k ⊆ v ⊆ R Cn S
6 4 5 elpwi2 ⊢ f ∈ R Cn S | f k ⊆ v ∈ 𝒫 R Cn S
7 6 rgen2w ⊢ ∀ k ∈ K ∀ v ∈ S f ∈ R Cn S | f k ⊆ v ∈ 𝒫 R Cn S
8 3 fmpo ⊢ ∀ k ∈ K ∀ v ∈ S f ∈ R Cn S | f k ⊆ v ∈ 𝒫 R Cn S ↔ T : K × S ⟶ 𝒫 R Cn S
9 7 8 mpbi ⊢ T : K × S ⟶ 𝒫 R Cn S