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