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 𝑇 ) ) )