This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xkoval

Description: Value of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses xkoval.x ⊢ 𝑋 = ∪ 𝑅
xkoval.k ⊢ 𝐾 = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp }
xkoval.t ⊢ 𝑇 = ( 𝑘 ∈ 𝐾 , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
Assertion xkoval ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 xkoval.x ⊢ 𝑋 = ∪ 𝑅
2 xkoval.k ⊢ 𝐾 = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp }
3 xkoval.t ⊢ 𝑇 = ( 𝑘 ∈ 𝐾 , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
4 simpr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
5 4 unieqd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ∪ 𝑟 = ∪ 𝑅 )
6 5 1 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ∪ 𝑟 = 𝑋 )
7 6 pweqd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → 𝒫 ∪ 𝑟 = 𝒫 𝑋 )
8 4 oveq1d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 𝑟 ↾t 𝑥 ) = ( 𝑅 ↾t 𝑥 ) )
9 8 eleq1d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( ( 𝑟 ↾t 𝑥 ) ∈ Comp ↔ ( 𝑅 ↾t 𝑥 ) ∈ Comp ) )
10 7 9 rabeqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } )
11 10 2 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } = 𝐾 )
12 simpl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → 𝑠 = 𝑆 )
13 4 12 oveq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 𝑟 Cn 𝑠 ) = ( 𝑅 Cn 𝑆 ) )
14 13 rabeqdv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
15 11 12 14 mpoeq123dv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ( 𝑘 ∈ 𝐾 , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
16 15 3 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = 𝑇 )
17 16 rneqd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ran 𝑇 )
18 17 fveq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) = ( fi ‘ ran 𝑇 ) )
19 18 fveq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) = ( topGen ‘ ( fi ‘ ran 𝑇 ) ) )
20 df-xko ⊢ ↑ko = ( 𝑠 ∈ Top , 𝑟 ∈ Top ↦ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
21 fvex ⊢ ( topGen ‘ ( fi ‘ ran 𝑇 ) ) ∈ V
22 19 20 21 ovmpoa ⊢ ( ( 𝑆 ∈ Top ∧ 𝑅 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran 𝑇 ) ) )
23 22 ancoms ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran 𝑇 ) ) )