Metamath Proof Explorer

Theorem xkoval

Description: Value of the compact-open topology. (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 xkoval ⊢ R ∈ Top ∧ S ∈ Top → S ^ ko R = topGen ⁡ fi ⁡ ran ⁡ T

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 simpr ⊢ s = S ∧ r = R → r = R
5 4 unieqd ⊢ s = S ∧ r = R → ⋃ r = ⋃ R
6 5 1 eqtr4di ⊢ s = S ∧ r = R → ⋃ r = X
7 6 pweqd ⊢ s = S ∧ r = R → 𝒫 ⋃ r = 𝒫 X
8 4 oveq1d ⊢ s = S ∧ r = R → r ↾ 𝑡 x = R ↾ 𝑡 x
9 8 eleq1d ⊢ s = S ∧ r = R → r ↾ 𝑡 x ∈ Comp ↔ R ↾ 𝑡 x ∈ Comp
10 7 9 rabeqbidv ⊢ s = S ∧ r = R → x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp = x ∈ 𝒫 X | R ↾ 𝑡 x ∈ Comp
11 10 2 eqtr4di ⊢ s = S ∧ r = R → x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp = K
12 simpl ⊢ s = S ∧ r = R → s = S
13 4 12 oveq12d ⊢ s = S ∧ r = R → r Cn s = R Cn S
14 13 rabeqdv ⊢ s = S ∧ r = R → f ∈ r Cn s | f k ⊆ v = f ∈ R Cn S | f k ⊆ v
15 11 12 14 mpoeq123dv ⊢ s = S ∧ r = R → k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v = k ∈ K , v ∈ S ⟼ f ∈ R Cn S | f k ⊆ v
16 15 3 eqtr4di ⊢ s = S ∧ r = R → k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v = T
17 16 rneqd ⊢ s = S ∧ r = R → ran ⁡ k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v = ran ⁡ T
18 17 fveq2d ⊢ s = S ∧ r = R → fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v = fi ⁡ ran ⁡ T
19 18 fveq2d ⊢ s = S ∧ r = R → topGen ⁡ fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v = topGen ⁡ fi ⁡ ran ⁡ T
20 df-xko ⊢ ^ ko = s ∈ Top , r ∈ Top ⟼ topGen ⁡ fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v
21 fvex ⊢ topGen ⁡ fi ⁡ ran ⁡ T ∈ V
22 19 20 21 ovmpoa ⊢ S ∈ Top ∧ R ∈ Top → S ^ ko R = topGen ⁡ fi ⁡ ran ⁡ T
23 22 ancoms ⊢ R ∈ Top ∧ S ∈ Top → S ^ ko R = topGen ⁡ fi ⁡ ran ⁡ T