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

Metamath Proof Explorer

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 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) }