xkouni

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

		Ref	Expression
	Hypothesis	xkouni.1	\|- J = ( S ^ko R )
	Assertion	xkouni	\|- ( ( R e. Top /\ S e. Top ) -> ( R Cn S ) = U. J )

Proof

Step	Hyp	Ref	Expression
1		xkouni.1	\|- J = ( S ^ko R )
2		ima0	\|- ( f " (/) ) = (/)
3		0ss	\|- (/) C_ U. S
4	2 3	eqsstri	\|- ( f " (/) ) C_ U. S
5	4	a1i	\|- ( ( ( R e. Top /\ S e. Top ) /\ f e. ( R Cn S ) ) -> ( f " (/) ) C_ U. S )
6	5	ralrimiva	\|- ( ( R e. Top /\ S e. Top ) -> A. f e. ( R Cn S ) ( f " (/) ) C_ U. S )
7		rabid2	\|- ( ( R Cn S ) = { f e. ( R Cn S ) \| ( f " (/) ) C_ U. S } <-> A. f e. ( R Cn S ) ( f " (/) ) C_ U. S )
8	6 7	sylibr	\|- ( ( R e. Top /\ S e. Top ) -> ( R Cn S ) = { f e. ( R Cn S ) \| ( f " (/) ) C_ U. S } )
9		eqid	\|- U. R = U. R
10		simpl	\|- ( ( R e. Top /\ S e. Top ) -> R e. Top )
11		simpr	\|- ( ( R e. Top /\ S e. Top ) -> S e. Top )
12		0ss	\|- (/) C_ U. R
13	12	a1i	\|- ( ( R e. Top /\ S e. Top ) -> (/) C_ U. R )
14		rest0	\|- ( R e. Top -> ( R \|`t (/) ) = { (/) } )
15	14	adantr	\|- ( ( R e. Top /\ S e. Top ) -> ( R \|`t (/) ) = { (/) } )
16		0cmp	\|- { (/) } e. Comp
17	15 16	eqeltrdi	\|- ( ( R e. Top /\ S e. Top ) -> ( R \|`t (/) ) e. Comp )
18		eqid	\|- U. S = U. S
19	18	topopn	\|- ( S e. Top -> U. S e. S )
20	19	adantl	\|- ( ( R e. Top /\ S e. Top ) -> U. S e. S )
21	9 10 11 13 17 20	xkoopn	\|- ( ( R e. Top /\ S e. Top ) -> { f e. ( R Cn S ) \| ( f " (/) ) C_ U. S } e. ( S ^ko R ) )
22	8 21	eqeltrd	\|- ( ( R e. Top /\ S e. Top ) -> ( R Cn S ) e. ( S ^ko R ) )
23	22 1	eleqtrrdi	\|- ( ( R e. Top /\ S e. Top ) -> ( R Cn S ) e. J )
24		elssuni	\|- ( ( R Cn S ) e. J -> ( R Cn S ) C_ U. J )
25	23 24	syl	\|- ( ( R e. Top /\ S e. Top ) -> ( R Cn S ) C_ U. J )
26		eqid	\|- { x e. ~P U. R \| ( R \|`t x ) e. Comp } = { x e. ~P U. R \| ( R \|`t x ) e. Comp }
27		eqid	\|- ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) = ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } )
28	9 26 27	xkoval	\|- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) = ( topGen ` ( fi ` ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) ) )
29	28	unieqd	\|- ( ( R e. Top /\ S e. Top ) -> U. ( S ^ko R ) = U. ( topGen ` ( fi ` ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) ) )
30	1	unieqi	\|- U. J = U. ( S ^ko R )
31		ovex	\|- ( R Cn S ) e. _V
32	31	pwex	\|- ~P ( R Cn S ) e. _V
33	9 26 27	xkotf	\|- ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) : ( { x e. ~P U. R \| ( R \|`t x ) e. Comp } X. S ) --> ~P ( R Cn S )
34		frn	\|- ( ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) : ( { x e. ~P U. R \| ( R \|`t x ) e. Comp } X. S ) --> ~P ( R Cn S ) -> ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) C_ ~P ( R Cn S ) )
35	33 34	ax-mp	\|- ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) C_ ~P ( R Cn S )
36	32 35	ssexi	\|- ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) e. _V
37		fiuni	\|- ( ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) e. _V -> U. ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) = U. ( fi ` ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) )
38	36 37	ax-mp	\|- U. ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) = U. ( fi ` ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) )
39		fvex	\|- ( fi ` ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) e. _V
40		unitg	\|- ( ( fi ` ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) e. _V -> U. ( topGen ` ( fi ` ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) ) = U. ( fi ` ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) )
41	39 40	ax-mp	\|- U. ( topGen ` ( fi ` ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) ) = U. ( fi ` ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) )
42	38 41	eqtr4i	\|- U. ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) = U. ( topGen ` ( fi ` ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) ) )
43	29 30 42	3eqtr4g	\|- ( ( R e. Top /\ S e. Top ) -> U. J = U. ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) )
44	35	a1i	\|- ( ( R e. Top /\ S e. Top ) -> ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) C_ ~P ( R Cn S ) )
45		sspwuni	\|- ( ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) C_ ~P ( R Cn S ) <-> U. ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) C_ ( R Cn S ) )
46	44 45	sylib	\|- ( ( R e. Top /\ S e. Top ) -> U. ran ( k e. { x e. ~P U. R \| ( R \|`t x ) e. Comp } , v e. S \|-> { f e. ( R Cn S ) \| ( f " k ) C_ v } ) C_ ( R Cn S ) )
47	43 46	eqsstrd	\|- ( ( R e. Top /\ S e. Top ) -> U. J C_ ( R Cn S ) )
48	25 47	eqssd	\|- ( ( R e. Top /\ S e. Top ) -> ( R Cn S ) = U. J )

Metamath Proof Explorer

Theorem xkouni

Proof