Theorem xkobval

Description: Alternative expression for the subbase of the compact-open topology. (Contributed by Mario Carneiro, 23-Mar-2015)

	Ref	Expression
Hypotheses	xkoval.x	⊢ 𝑋 = ∪ 𝑅
	xkoval.k	⊢ 𝐾 = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp }
	xkoval.t	⊢ 𝑇 = ( 𝑘 ∈ 𝐾 , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
Assertion	xkobval	⊢ ran 𝑇 = { 𝑠 ∣ ∃ 𝑘 ∈ 𝒫 𝑋 ∃ 𝑣 ∈ 𝑆 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) }

Proof

Step	Hyp	Ref	Expression
1		xkoval.x	⊢ 𝑋 = ∪ 𝑅
2		xkoval.k	⊢ 𝐾 = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp }
3		xkoval.t	⊢ 𝑇 = ( 𝑘 ∈ 𝐾 , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
4	3	rnmpo	⊢ ran 𝑇 = { 𝑠 ∣ ∃ 𝑘 ∈ 𝐾 ∃ 𝑣 ∈ 𝑆 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } }
5		oveq2	⊢ ( 𝑥 = 𝑘 → ( 𝑅 ↾t 𝑥 ) = ( 𝑅 ↾t 𝑘 ) )
6	5	eleq1d	⊢ ( 𝑥 = 𝑘 → ( ( 𝑅 ↾t 𝑥 ) ∈ Comp ↔ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) )
7	6	rexrab	⊢ ( ∃ 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } ∃ 𝑣 ∈ 𝑆 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ↔ ∃ 𝑘 ∈ 𝒫 𝑋 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ ∃ 𝑣 ∈ 𝑆 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
8	2	rexeqi	⊢ ( ∃ 𝑘 ∈ 𝐾 ∃ 𝑣 ∈ 𝑆 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ↔ ∃ 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } ∃ 𝑣 ∈ 𝑆 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
9		r19.42v	⊢ ( ∃ 𝑣 ∈ 𝑆 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ↔ ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ ∃ 𝑣 ∈ 𝑆 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
10	9	rexbii	⊢ ( ∃ 𝑘 ∈ 𝒫 𝑋 ∃ 𝑣 ∈ 𝑆 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ↔ ∃ 𝑘 ∈ 𝒫 𝑋 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ ∃ 𝑣 ∈ 𝑆 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
11	7 8 10	3bitr4i	⊢ ( ∃ 𝑘 ∈ 𝐾 ∃ 𝑣 ∈ 𝑆 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ↔ ∃ 𝑘 ∈ 𝒫 𝑋 ∃ 𝑣 ∈ 𝑆 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
12	11	abbii	⊢ { 𝑠 ∣ ∃ 𝑘 ∈ 𝐾 ∃ 𝑣 ∈ 𝑆 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } = { 𝑠 ∣ ∃ 𝑘 ∈ 𝒫 𝑋 ∃ 𝑣 ∈ 𝑆 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) }
13	4 12	eqtri	⊢ ran 𝑇 = { 𝑠 ∣ ∃ 𝑘 ∈ 𝒫 𝑋 ∃ 𝑣 ∈ 𝑆 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑠 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) }