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 
|- X = U. R
xkoval.k 
|- K = { x e. ~P X | ( R |`t x ) e. Comp }
xkoval.t 
|- T = ( k e. K , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } )
Assertion xkobval 
|- ran T = { s | E. k e. ~P X E. v e. S ( ( R |`t k ) e. Comp /\ s = { f e. ( R Cn S ) | ( f " k ) C_ v } ) }

Proof

Step Hyp Ref Expression
1 xkoval.x 
 |-  X = U. R
2 xkoval.k 
 |-  K = { x e. ~P X | ( R |`t x ) e. Comp }
3 xkoval.t 
 |-  T = ( k e. K , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } )
4 3 rnmpo 
 |-  ran T = { s | E. k e. K E. v e. S s = { f e. ( R Cn S ) | ( f " k ) C_ v } }
5 oveq2 
 |-  ( x = k -> ( R |`t x ) = ( R |`t k ) )
6 5 eleq1d 
 |-  ( x = k -> ( ( R |`t x ) e. Comp <-> ( R |`t k ) e. Comp ) )
7 6 rexrab 
 |-  ( E. k e. { x e. ~P X | ( R |`t x ) e. Comp } E. v e. S s = { f e. ( R Cn S ) | ( f " k ) C_ v } <-> E. k e. ~P X ( ( R |`t k ) e. Comp /\ E. v e. S s = { f e. ( R Cn S ) | ( f " k ) C_ v } ) )
8 2 rexeqi 
 |-  ( E. k e. K E. v e. S s = { f e. ( R Cn S ) | ( f " k ) C_ v } <-> E. k e. { x e. ~P X | ( R |`t x ) e. Comp } E. v e. S s = { f e. ( R Cn S ) | ( f " k ) C_ v } )
9 r19.42v 
 |-  ( E. v e. S ( ( R |`t k ) e. Comp /\ s = { f e. ( R Cn S ) | ( f " k ) C_ v } ) <-> ( ( R |`t k ) e. Comp /\ E. v e. S s = { f e. ( R Cn S ) | ( f " k ) C_ v } ) )
10 9 rexbii 
 |-  ( E. k e. ~P X E. v e. S ( ( R |`t k ) e. Comp /\ s = { f e. ( R Cn S ) | ( f " k ) C_ v } ) <-> E. k e. ~P X ( ( R |`t k ) e. Comp /\ E. v e. S s = { f e. ( R Cn S ) | ( f " k ) C_ v } ) )
11 7 8 10 3bitr4i 
 |-  ( E. k e. K E. v e. S s = { f e. ( R Cn S ) | ( f " k ) C_ v } <-> E. k e. ~P X E. v e. S ( ( R |`t k ) e. Comp /\ s = { f e. ( R Cn S ) | ( f " k ) C_ v } ) )
12 11 abbii 
 |-  { s | E. k e. K E. v e. S s = { f e. ( R Cn S ) | ( f " k ) C_ v } } = { s | E. k e. ~P X E. v e. S ( ( R |`t k ) e. Comp /\ s = { f e. ( R Cn S ) | ( f " k ) C_ v } ) }
13 4 12 eqtri 
 |-  ran T = { s | E. k e. ~P X E. v e. S ( ( R |`t k ) e. Comp /\ s = { f e. ( R Cn S ) | ( f " k ) C_ v } ) }