xkoopn

Description: A basic open set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015)

	Ref	Expression
Hypotheses	xkoopn.x	\|- X = U. R
	xkoopn.r	\|- ( ph -> R e. Top )
	xkoopn.s	\|- ( ph -> S e. Top )
	xkoopn.a	\|- ( ph -> A C_ X )
	xkoopn.c	\|- ( ph -> ( R \|`t A ) e. Comp )
	xkoopn.u	\|- ( ph -> U e. S )
Assertion	xkoopn	\|- ( ph -> { f e. ( R Cn S ) \| ( f " A ) C_ U } e. ( S ^ko R ) )

Proof

Step	Hyp	Ref	Expression
1		xkoopn.x	\|- X = U. R
2		xkoopn.r	\|- ( ph -> R e. Top )
3		xkoopn.s	\|- ( ph -> S e. Top )
4		xkoopn.a	\|- ( ph -> A C_ X )
5		xkoopn.c	\|- ( ph -> ( R \|`t A ) e. Comp )
6		xkoopn.u	\|- ( ph -> U e. S )
7		ovex	\|- ( R Cn S ) e. _V
8	7	pwex	\|- ~P ( R Cn S ) e. _V
9		eqid	\|- { x e. ~P X \| ( R \|`t x ) e. Comp } = { x e. ~P X \| ( R \|`t x ) e. Comp }
10		eqid	\|- ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) = ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } )
11	1 9 10	xkotf	\|- ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) : ( { x e. ~P X \| ( R \|`t x ) e. Comp } X. S ) --> ~P ( R Cn S )
12		frn	\|- ( ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) : ( { x e. ~P X \| ( R \|`t x ) e. Comp } X. S ) --> ~P ( R Cn S ) -> ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) C_ ~P ( R Cn S ) )
13	11 12	ax-mp	\|- ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) C_ ~P ( R Cn S )
14	8 13	ssexi	\|- ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) e. _V
15		ssfii	\|- ( ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) e. _V -> ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) C_ ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) )
16	14 15	ax-mp	\|- ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) C_ ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) )
17		fvex	\|- ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) e. _V
18		bastg	\|- ( ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) e. _V -> ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) C_ ( topGen ` ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) ) )
19	17 18	ax-mp	\|- ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) C_ ( topGen ` ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) )
20	16 19	sstri	\|- ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) C_ ( topGen ` ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) )
21		oveq2	\|- ( x = A -> ( R \|`t x ) = ( R \|`t A ) )
22	21	eleq1d	\|- ( x = A -> ( ( R \|`t x ) e. Comp <-> ( R \|`t A ) e. Comp ) )
23	1	topopn	\|- ( R e. Top -> X e. R )
24		elpw2g	\|- ( X e. R -> ( A e. ~P X <-> A C_ X ) )
25	2 23 24	3syl	\|- ( ph -> ( A e. ~P X <-> A C_ X ) )
26	4 25	mpbird	\|- ( ph -> A e. ~P X )
27	22 26 5	elrabd	\|- ( ph -> A e. { x e. ~P X \| ( R \|`t x ) e. Comp } )
28		eqidd	\|- ( ph -> { f e. ( R Cn S ) \| ( f " A ) C_ U } = { f e. ( R Cn S ) \| ( f " A ) C_ U } )
29		imaeq2	\|- ( k = A -> ( f " k ) = ( f " A ) )
30	29	sseq1d	\|- ( k = A -> ( ( f " k ) C_ v <-> ( f " A ) C_ v ) )
31	30	rabbidv	\|- ( k = A -> { f e. ( R Cn S ) \| ( f " k ) C_ v } = { f e. ( R Cn S ) \| ( f " A ) C_ v } )
32	31	eqeq2d	\|- ( k = A -> ( { f e. ( R Cn S ) \| ( f " A ) C_ U } = { f e. ( R Cn S ) \| ( f " k ) C_ v } <-> { f e. ( R Cn S ) \| ( f " A ) C_ U } = { f e. ( R Cn S ) \| ( f " A ) C_ v } ) )
33		sseq2	\|- ( v = U -> ( ( f " A ) C_ v <-> ( f " A ) C_ U ) )
34	33	rabbidv	\|- ( v = U -> { f e. ( R Cn S ) \| ( f " A ) C_ v } = { f e. ( R Cn S ) \| ( f " A ) C_ U } )
35	34	eqeq2d	\|- ( v = U -> ( { f e. ( R Cn S ) \| ( f " A ) C_ U } = { f e. ( R Cn S ) \| ( f " A ) C_ v } <-> { f e. ( R Cn S ) \| ( f " A ) C_ U } = { f e. ( R Cn S ) \| ( f " A ) C_ U } ) )
36	32 35	rspc2ev	\|- ( ( A e. { x e. ~P X \| ( R \|`t x ) e. Comp } /\ U e. S /\ { f e. ( R Cn S ) \| ( f " A ) C_ U } = { f e. ( R Cn S ) \| ( f " A ) C_ U } ) -> E. k e. { x e. ~P X \| ( R \|`t x ) e. Comp } E. v e. S { f e. ( R Cn S ) \| ( f " A ) C_ U } = { f e. ( R Cn S ) \| ( f " k ) C_ v } )
37	27 6 28 36	syl3anc	\|- ( ph -> E. k e. { x e. ~P X \| ( R \|`t x ) e. Comp } E. v e. S { f e. ( R Cn S ) \| ( f " A ) C_ U } = { f e. ( R Cn S ) \| ( f " k ) C_ v } )
38	7	rabex	\|- { f e. ( R Cn S ) \| ( f " A ) C_ U } e. _V
39		eqeq1	\|- ( y = { f e. ( R Cn S ) \| ( f " A ) C_ U } -> ( y = { f e. ( R Cn S ) \| ( f " k ) C_ v } <-> { f e. ( R Cn S ) \| ( f " A ) C_ U } = { f e. ( R Cn S ) \| ( f " k ) C_ v } ) )
40	39	2rexbidv	\|- ( y = { f e. ( R Cn S ) \| ( f " A ) C_ U } -> ( E. k e. { x e. ~P X \| ( R \|`t x ) e. Comp } E. v e. S y = { 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 { f e. ( R Cn S ) \| ( f " A ) C_ U } = { f e. ( R Cn S ) \| ( f " k ) C_ v } ) )
41	10	rnmpo	\|- ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) = { y \| E. k e. { x e. ~P X \| ( R \|`t x ) e. Comp } E. v e. S y = { f e. ( R Cn S ) \| ( f " k ) C_ v } }
42	38 40 41	elab2	\|- ( { f e. ( R Cn S ) \| ( f " A ) C_ U } e. ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. 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 { f e. ( R Cn S ) \| ( f " A ) C_ U } = { f e. ( R Cn S ) \| ( f " k ) C_ v } )
43	37 42	sylibr	\|- ( ph -> { f e. ( R Cn S ) \| ( f " A ) C_ U } e. ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) )
44	20 43	sseldi	\|- ( ph -> { f e. ( R Cn S ) \| ( f " A ) C_ U } e. ( topGen ` ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) ) )
45	1 9 10	xkoval	\|- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) = ( topGen ` ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) ) )
46	2 3 45	syl2anc	\|- ( ph -> ( S ^ko R ) = ( topGen ` ( fi ` ran ( k e. { x e. ~P X \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) ) )
47	44 46	eleqtrrd	\|- ( ph -> { f e. ( R Cn S ) \| ( f " A ) C_ U } e. ( S ^ko R ) )

Metamath Proof Explorer

Theorem xkoopn

Proof