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

Metamath Proof Explorer

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