Metamath Proof Explorer

Theorem xkoptsub

Description: The compact-open topology is finer than the product topology restricted to continuous functions. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses xkoptsub.x 
|- X = U. R
xkoptsub.j 
|- J = ( Xt_ ` ( X X. { S } ) )
Assertion xkoptsub 
|- ( ( R e. Top /\ S e. Top ) -> ( J |`t ( R Cn S ) ) C_ ( S ^ko R ) )

Proof

Step Hyp Ref Expression
1 xkoptsub.x 
 |-  X = U. R
2 xkoptsub.j 
 |-  J = ( Xt_ ` ( X X. { S } ) )
3 1 topopn 
 |-  ( R e. Top -> X e. R )
4 3 adantr 
 |-  ( ( R e. Top /\ S e. Top ) -> X e. R )
5 fconstg 
 |-  ( S e. Top -> ( X X. { S } ) : X --> { S } )
6 5 adantl 
 |-  ( ( R e. Top /\ S e. Top ) -> ( X X. { S } ) : X --> { S } )
7 6 ffnd 
 |-  ( ( R e. Top /\ S e. Top ) -> ( X X. { S } ) Fn X )
8 eqid 
 |-  { x | E. g ( ( g Fn X /\ A. y e. X ( g ` y ) e. ( ( X X. { S } ) ` y ) /\ E. z e. Fin A. y e. ( X \ z ) ( g ` y ) = U. ( ( X X. { S } ) ` y ) ) /\ x = X_ y e. X ( g ` y ) ) } = { x | E. g ( ( g Fn X /\ A. y e. X ( g ` y ) e. ( ( X X. { S } ) ` y ) /\ E. z e. Fin A. y e. ( X \ z ) ( g ` y ) = U. ( ( X X. { S } ) ` y ) ) /\ x = X_ y e. X ( g ` y ) ) }
9 8 ptval 
 |-  ( ( X e. R /\ ( X X. { S } ) Fn X ) -> ( Xt_ ` ( X X. { S } ) ) = ( topGen ` { x | E. g ( ( g Fn X /\ A. y e. X ( g ` y ) e. ( ( X X. { S } ) ` y ) /\ E. z e. Fin A. y e. ( X \ z ) ( g ` y ) = U. ( ( X X. { S } ) ` y ) ) /\ x = X_ y e. X ( g ` y ) ) } ) )
10 4 7 9 syl2anc 
 |-  ( ( R e. Top /\ S e. Top ) -> ( Xt_ ` ( X X. { S } ) ) = ( topGen ` { x | E. g ( ( g Fn X /\ A. y e. X ( g ` y ) e. ( ( X X. { S } ) ` y ) /\ E. z e. Fin A. y e. ( X \ z ) ( g ` y ) = U. ( ( X X. { S } ) ` y ) ) /\ x = X_ y e. X ( g ` y ) ) } ) )
11 simpr 
 |-  ( ( R e. Top /\ S e. Top ) -> S e. Top )
12 11 snssd 
 |-  ( ( R e. Top /\ S e. Top ) -> { S } C_ Top )
13 6 12 fssd 
 |-  ( ( R e. Top /\ S e. Top ) -> ( X X. { S } ) : X --> Top )
14 eqid 
 |-  X_ n e. X U. ( ( X X. { S } ) ` n ) = X_ n e. X U. ( ( X X. { S } ) ` n )
15 8 14 ptbasfi 
 |-  ( ( X e. R /\ ( X X. { S } ) : X --> Top ) -> { x | E. g ( ( g Fn X /\ A. y e. X ( g ` y ) e. ( ( X X. { S } ) ` y ) /\ E. z e. Fin A. y e. ( X \ z ) ( g ` y ) = U. ( ( X X. { S } ) ` y ) ) /\ x = X_ y e. X ( g ` y ) ) } = ( fi ` ( { X_ n e. X U. ( ( X X. { S } ) ` n ) } u. ran ( k e. X , u e. ( ( X X. { S } ) ` k ) |-> ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) ) ) ) )
16 4 13 15 syl2anc 
 |-  ( ( R e. Top /\ S e. Top ) -> { x | E. g ( ( g Fn X /\ A. y e. X ( g ` y ) e. ( ( X X. { S } ) ` y ) /\ E. z e. Fin A. y e. ( X \ z ) ( g ` y ) = U. ( ( X X. { S } ) ` y ) ) /\ x = X_ y e. X ( g ` y ) ) } = ( fi ` ( { X_ n e. X U. ( ( X X. { S } ) ` n ) } u. ran ( k e. X , u e. ( ( X X. { S } ) ` k ) |-> ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) ) ) ) )
17 fvconst2g 
 |-  ( ( S e. Top /\ n e. X ) -> ( ( X X. { S } ) ` n ) = S )
18 17 adantll 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ n e. X ) -> ( ( X X. { S } ) ` n ) = S )
19 18 unieqd 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ n e. X ) -> U. ( ( X X. { S } ) ` n ) = U. S )
20 19 ixpeq2dva 
 |-  ( ( R e. Top /\ S e. Top ) -> X_ n e. X U. ( ( X X. { S } ) ` n ) = X_ n e. X U. S )
21 eqid 
 |-  U. S = U. S
22 21 topopn 
 |-  ( S e. Top -> U. S e. S )
23 ixpconstg 
 |-  ( ( X e. R /\ U. S e. S ) -> X_ n e. X U. S = ( U. S ^m X ) )
24 3 22 23 syl2an 
 |-  ( ( R e. Top /\ S e. Top ) -> X_ n e. X U. S = ( U. S ^m X ) )
25 20 24 eqtrd 
 |-  ( ( R e. Top /\ S e. Top ) -> X_ n e. X U. ( ( X X. { S } ) ` n ) = ( U. S ^m X ) )
26 25 sneqd 
 |-  ( ( R e. Top /\ S e. Top ) -> { X_ n e. X U. ( ( X X. { S } ) ` n ) } = { ( U. S ^m X ) } )
27 eqid 
 |-  X = X
28 fvconst2g 
 |-  ( ( S e. Top /\ k e. X ) -> ( ( X X. { S } ) ` k ) = S )
29 28 adantll 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ k e. X ) -> ( ( X X. { S } ) ` k ) = S )
30 25 adantr 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ k e. X ) -> X_ n e. X U. ( ( X X. { S } ) ` n ) = ( U. S ^m X ) )
31 30 mpteq1d 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ k e. X ) -> ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) = ( w e. ( U. S ^m X ) |-> ( w ` k ) ) )
32 31 cnveqd 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ k e. X ) -> `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) = `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) )
33 32 imaeq1d 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ k e. X ) -> ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) )
34 33 ralrimivw 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ k e. X ) -> A. u e. ( ( X X. { S } ) ` k ) ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) )
35 29 34 jca 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ k e. X ) -> ( ( ( X X. { S } ) ` k ) = S /\ A. u e. ( ( X X. { S } ) ` k ) ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) )
36 35 ralrimiva 
 |-  ( ( R e. Top /\ S e. Top ) -> A. k e. X ( ( ( X X. { S } ) ` k ) = S /\ A. u e. ( ( X X. { S } ) ` k ) ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) )
37 mpoeq123 
 |-  ( ( X = X /\ A. k e. X ( ( ( X X. { S } ) ` k ) = S /\ A. u e. ( ( X X. { S } ) ` k ) ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) -> ( k e. X , u e. ( ( X X. { S } ) ` k ) |-> ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) ) = ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) )
38 27 36 37 sylancr 
 |-  ( ( R e. Top /\ S e. Top ) -> ( k e. X , u e. ( ( X X. { S } ) ` k ) |-> ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) ) = ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) )
39 38 rneqd 
 |-  ( ( R e. Top /\ S e. Top ) -> ran ( k e. X , u e. ( ( X X. { S } ) ` k ) |-> ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) ) = ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) )
40 26 39 uneq12d 
 |-  ( ( R e. Top /\ S e. Top ) -> ( { X_ n e. X U. ( ( X X. { S } ) ` n ) } u. ran ( k e. X , u e. ( ( X X. { S } ) ` k ) |-> ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) ) ) = ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) )
41 40 fveq2d 
 |-  ( ( R e. Top /\ S e. Top ) -> ( fi ` ( { X_ n e. X U. ( ( X X. { S } ) ` n ) } u. ran ( k e. X , u e. ( ( X X. { S } ) ` k ) |-> ( `' ( w e. X_ n e. X U. ( ( X X. { S } ) ` n ) |-> ( w ` k ) ) " u ) ) ) ) = ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) )
42 16 41 eqtrd 
 |-  ( ( R e. Top /\ S e. Top ) -> { x | E. g ( ( g Fn X /\ A. y e. X ( g ` y ) e. ( ( X X. { S } ) ` y ) /\ E. z e. Fin A. y e. ( X \ z ) ( g ` y ) = U. ( ( X X. { S } ) ` y ) ) /\ x = X_ y e. X ( g ` y ) ) } = ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) )
43 42 fveq2d 
 |-  ( ( R e. Top /\ S e. Top ) -> ( topGen ` { x | E. g ( ( g Fn X /\ A. y e. X ( g ` y ) e. ( ( X X. { S } ) ` y ) /\ E. z e. Fin A. y e. ( X \ z ) ( g ` y ) = U. ( ( X X. { S } ) ` y ) ) /\ x = X_ y e. X ( g ` y ) ) } ) = ( topGen ` ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) ) )
44 10 43 eqtrd 
 |-  ( ( R e. Top /\ S e. Top ) -> ( Xt_ ` ( X X. { S } ) ) = ( topGen ` ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) ) )
45 2 44 syl5eq 
 |-  ( ( R e. Top /\ S e. Top ) -> J = ( topGen ` ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) ) )
46 45 oveq1d 
 |-  ( ( R e. Top /\ S e. Top ) -> ( J |`t ( R Cn S ) ) = ( ( topGen ` ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) ) |`t ( R Cn S ) ) )
47 firest 
 |-  ( fi ` ( ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |`t ( R Cn S ) ) ) = ( ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) |`t ( R Cn S ) )
48 47 fveq2i 
 |-  ( topGen ` ( fi ` ( ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |`t ( R Cn S ) ) ) ) = ( topGen ` ( ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) |`t ( R Cn S ) ) )
49 fvex 
 |-  ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) e. _V
50 ovex 
 |-  ( R Cn S ) e. _V
51 tgrest 
 |-  ( ( ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) e. _V /\ ( R Cn S ) e. _V ) -> ( topGen ` ( ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) |`t ( R Cn S ) ) ) = ( ( topGen ` ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) ) |`t ( R Cn S ) ) )
52 49 50 51 mp2an 
 |-  ( topGen ` ( ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) |`t ( R Cn S ) ) ) = ( ( topGen ` ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) ) |`t ( R Cn S ) )
53 48 52 eqtri 
 |-  ( topGen ` ( fi ` ( ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |`t ( R Cn S ) ) ) ) = ( ( topGen ` ( fi ` ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) ) |`t ( R Cn S ) )
54 46 53 eqtr4di 
 |-  ( ( R e. Top /\ S e. Top ) -> ( J |`t ( R Cn S ) ) = ( topGen ` ( fi ` ( ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |`t ( R Cn S ) ) ) ) )
55 xkotop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. Top )
56 snex 
 |-  { ( U. S ^m X ) } e. _V
57 mpoexga 
 |-  ( ( X e. R /\ S e. Top ) -> ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) e. _V )
58 3 57 sylan 
 |-  ( ( R e. Top /\ S e. Top ) -> ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) e. _V )
59 rnexg 
 |-  ( ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) e. _V -> ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) e. _V )
60 58 59 syl 
 |-  ( ( R e. Top /\ S e. Top ) -> ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) e. _V )
61 unexg 
 |-  ( ( { ( U. S ^m X ) } e. _V /\ ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) e. _V ) -> ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) e. _V )
62 56 60 61 sylancr 
 |-  ( ( R e. Top /\ S e. Top ) -> ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) e. _V )
63 restval 
 |-  ( ( ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) e. _V /\ ( R Cn S ) e. _V ) -> ( ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |`t ( R Cn S ) ) = ran ( x e. ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |-> ( x i^i ( R Cn S ) ) ) )
64 62 50 63 sylancl 
 |-  ( ( R e. Top /\ S e. Top ) -> ( ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |`t ( R Cn S ) ) = ran ( x e. ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |-> ( x i^i ( R Cn S ) ) ) )
65 elun 
 |-  ( x e. ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) <-> ( x e. { ( U. S ^m X ) } \/ x e. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) )
66 1 21 cnf 
 |-  ( x e. ( R Cn S ) -> x : X --> U. S )
67 elmapg 
 |-  ( ( U. S e. S /\ X e. R ) -> ( x e. ( U. S ^m X ) <-> x : X --> U. S ) )
68 22 3 67 syl2anr 
 |-  ( ( R e. Top /\ S e. Top ) -> ( x e. ( U. S ^m X ) <-> x : X --> U. S ) )
69 66 68 syl5ibr 
 |-  ( ( R e. Top /\ S e. Top ) -> ( x e. ( R Cn S ) -> x e. ( U. S ^m X ) ) )
70 69 ssrdv 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R Cn S ) C_ ( U. S ^m X ) )
71 70 adantr 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ x e. { ( U. S ^m X ) } ) -> ( R Cn S ) C_ ( U. S ^m X ) )
72 elsni 
 |-  ( x e. { ( U. S ^m X ) } -> x = ( U. S ^m X ) )
73 72 adantl 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ x e. { ( U. S ^m X ) } ) -> x = ( U. S ^m X ) )
74 71 73 sseqtrrd 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ x e. { ( U. S ^m X ) } ) -> ( R Cn S ) C_ x )
75 sseqin2 
 |-  ( ( R Cn S ) C_ x <-> ( x i^i ( R Cn S ) ) = ( R Cn S ) )
76 74 75 sylib 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ x e. { ( U. S ^m X ) } ) -> ( x i^i ( R Cn S ) ) = ( R Cn S ) )
77 eqid 
 |-  ( S ^ko R ) = ( S ^ko R )
78 77 xkouni 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R Cn S ) = U. ( S ^ko R ) )
79 eqid 
 |-  U. ( S ^ko R ) = U. ( S ^ko R )
80 79 topopn 
 |-  ( ( S ^ko R ) e. Top -> U. ( S ^ko R ) e. ( S ^ko R ) )
81 55 80 syl 
 |-  ( ( R e. Top /\ S e. Top ) -> U. ( S ^ko R ) e. ( S ^ko R ) )
82 78 81 eqeltrd 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R Cn S ) e. ( S ^ko R ) )
83 82 adantr 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ x e. { ( U. S ^m X ) } ) -> ( R Cn S ) e. ( S ^ko R ) )
84 76 83 eqeltrd 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ x e. { ( U. S ^m X ) } ) -> ( x i^i ( R Cn S ) ) e. ( S ^ko R ) )
85 eqid 
 |-  ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) = ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) )
86 85 rnmpo 
 |-  ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) = { x | E. k e. X E. u e. S x = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) }
87 86 abeq2i 
 |-  ( x e. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) <-> E. k e. X E. u e. S x = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) )
88 cnvresima 
 |-  ( `' ( ( w e. ( U. S ^m X ) |-> ( w ` k ) ) |` ( R Cn S ) ) " u ) = ( ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) i^i ( R Cn S ) )
89 70 adantr 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( R Cn S ) C_ ( U. S ^m X ) )
90 89 resmptd 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( ( w e. ( U. S ^m X ) |-> ( w ` k ) ) |` ( R Cn S ) ) = ( w e. ( R Cn S ) |-> ( w ` k ) ) )
91 90 cnveqd 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> `' ( ( w e. ( U. S ^m X ) |-> ( w ` k ) ) |` ( R Cn S ) ) = `' ( w e. ( R Cn S ) |-> ( w ` k ) ) )
92 91 imaeq1d 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( `' ( ( w e. ( U. S ^m X ) |-> ( w ` k ) ) |` ( R Cn S ) ) " u ) = ( `' ( w e. ( R Cn S ) |-> ( w ` k ) ) " u ) )
93 88 92 eqtr3id 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) i^i ( R Cn S ) ) = ( `' ( w e. ( R Cn S ) |-> ( w ` k ) ) " u ) )
94 fvex 
 |-  ( w ` k ) e. _V
95 94 rgenw 
 |-  A. w e. ( R Cn S ) ( w ` k ) e. _V
96 eqid 
 |-  ( w e. ( R Cn S ) |-> ( w ` k ) ) = ( w e. ( R Cn S ) |-> ( w ` k ) )
97 96 fnmpt 
 |-  ( A. w e. ( R Cn S ) ( w ` k ) e. _V -> ( w e. ( R Cn S ) |-> ( w ` k ) ) Fn ( R Cn S ) )
98 95 97 mp1i 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( w e. ( R Cn S ) |-> ( w ` k ) ) Fn ( R Cn S ) )
99 elpreima 
 |-  ( ( w e. ( R Cn S ) |-> ( w ` k ) ) Fn ( R Cn S ) -> ( f e. ( `' ( w e. ( R Cn S ) |-> ( w ` k ) ) " u ) <-> ( f e. ( R Cn S ) /\ ( ( w e. ( R Cn S ) |-> ( w ` k ) ) ` f ) e. u ) ) )
100 98 99 syl 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( f e. ( `' ( w e. ( R Cn S ) |-> ( w ` k ) ) " u ) <-> ( f e. ( R Cn S ) /\ ( ( w e. ( R Cn S ) |-> ( w ` k ) ) ` f ) e. u ) ) )
101 fveq1 
 |-  ( w = f -> ( w ` k ) = ( f ` k ) )
102 fvex 
 |-  ( f ` k ) e. _V
103 101 96 102 fvmpt 
 |-  ( f e. ( R Cn S ) -> ( ( w e. ( R Cn S ) |-> ( w ` k ) ) ` f ) = ( f ` k ) )
104 103 adantl 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) /\ f e. ( R Cn S ) ) -> ( ( w e. ( R Cn S ) |-> ( w ` k ) ) ` f ) = ( f ` k ) )
105 104 eleq1d 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) /\ f e. ( R Cn S ) ) -> ( ( ( w e. ( R Cn S ) |-> ( w ` k ) ) ` f ) e. u <-> ( f ` k ) e. u ) )
106 102 snss 
 |-  ( ( f ` k ) e. u <-> { ( f ` k ) } C_ u )
107 89 sselda 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) /\ f e. ( R Cn S ) ) -> f e. ( U. S ^m X ) )
108 elmapi 
 |-  ( f e. ( U. S ^m X ) -> f : X --> U. S )
109 ffn 
 |-  ( f : X --> U. S -> f Fn X )
110 107 108 109 3syl 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) /\ f e. ( R Cn S ) ) -> f Fn X )
111 simplrl 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) /\ f e. ( R Cn S ) ) -> k e. X )
112 fnsnfv 
 |-  ( ( f Fn X /\ k e. X ) -> { ( f ` k ) } = ( f " { k } ) )
113 110 111 112 syl2anc 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) /\ f e. ( R Cn S ) ) -> { ( f ` k ) } = ( f " { k } ) )
114 113 sseq1d 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) /\ f e. ( R Cn S ) ) -> ( { ( f ` k ) } C_ u <-> ( f " { k } ) C_ u ) )
115 106 114 syl5bb 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) /\ f e. ( R Cn S ) ) -> ( ( f ` k ) e. u <-> ( f " { k } ) C_ u ) )
116 105 115 bitrd 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) /\ f e. ( R Cn S ) ) -> ( ( ( w e. ( R Cn S ) |-> ( w ` k ) ) ` f ) e. u <-> ( f " { k } ) C_ u ) )
117 116 pm5.32da 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( ( f e. ( R Cn S ) /\ ( ( w e. ( R Cn S ) |-> ( w ` k ) ) ` f ) e. u ) <-> ( f e. ( R Cn S ) /\ ( f " { k } ) C_ u ) ) )
118 100 117 bitrd 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( f e. ( `' ( w e. ( R Cn S ) |-> ( w ` k ) ) " u ) <-> ( f e. ( R Cn S ) /\ ( f " { k } ) C_ u ) ) )
119 118 abbi2dv 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( `' ( w e. ( R Cn S ) |-> ( w ` k ) ) " u ) = { f | ( f e. ( R Cn S ) /\ ( f " { k } ) C_ u ) } )
120 df-rab 
 |-  { f e. ( R Cn S ) | ( f " { k } ) C_ u } = { f | ( f e. ( R Cn S ) /\ ( f " { k } ) C_ u ) }
121 119 120 eqtr4di 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( `' ( w e. ( R Cn S ) |-> ( w ` k ) ) " u ) = { f e. ( R Cn S ) | ( f " { k } ) C_ u } )
122 93 121 eqtrd 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) i^i ( R Cn S ) ) = { f e. ( R Cn S ) | ( f " { k } ) C_ u } )
123 simpll 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> R e. Top )
124 11 adantr 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> S e. Top )
125 simprl 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> k e. X )
126 125 snssd 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> { k } C_ X )
127 1 toptopon 
 |-  ( R e. Top <-> R e. ( TopOn ` X ) )
128 123 127 sylib 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> R e. ( TopOn ` X ) )
129 restsn2 
 |-  ( ( R e. ( TopOn ` X ) /\ k e. X ) -> ( R |`t { k } ) = ~P { k } )
130 128 125 129 syl2anc 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( R |`t { k } ) = ~P { k } )
131 snfi 
 |-  { k } e. Fin
132 discmp 
 |-  ( { k } e. Fin <-> ~P { k } e. Comp )
133 131 132 mpbi 
 |-  ~P { k } e. Comp
134 130 133 eqeltrdi 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( R |`t { k } ) e. Comp )
135 simprr 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> u e. S )
136 1 123 124 126 134 135 xkoopn 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> { f e. ( R Cn S ) | ( f " { k } ) C_ u } e. ( S ^ko R ) )
137 122 136 eqeltrd 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) i^i ( R Cn S ) ) e. ( S ^ko R ) )
138 ineq1 
 |-  ( x = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) -> ( x i^i ( R Cn S ) ) = ( ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) i^i ( R Cn S ) ) )
139 138 eleq1d 
 |-  ( x = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) -> ( ( x i^i ( R Cn S ) ) e. ( S ^ko R ) <-> ( ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) i^i ( R Cn S ) ) e. ( S ^ko R ) ) )
140 137 139 syl5ibrcom 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( k e. X /\ u e. S ) ) -> ( x = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) -> ( x i^i ( R Cn S ) ) e. ( S ^ko R ) ) )
141 140 rexlimdvva 
 |-  ( ( R e. Top /\ S e. Top ) -> ( E. k e. X E. u e. S x = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) -> ( x i^i ( R Cn S ) ) e. ( S ^ko R ) ) )
142 141 imp 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ E. k e. X E. u e. S x = ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) -> ( x i^i ( R Cn S ) ) e. ( S ^ko R ) )
143 87 142 sylan2b 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ x e. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) -> ( x i^i ( R Cn S ) ) e. ( S ^ko R ) )
144 84 143 jaodan 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( x e. { ( U. S ^m X ) } \/ x e. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) -> ( x i^i ( R Cn S ) ) e. ( S ^ko R ) )
145 65 144 sylan2b 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ x e. ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) ) -> ( x i^i ( R Cn S ) ) e. ( S ^ko R ) )
146 145 fmpttd 
 |-  ( ( R e. Top /\ S e. Top ) -> ( x e. ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |-> ( x i^i ( R Cn S ) ) ) : ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) --> ( S ^ko R ) )
147 146 frnd 
 |-  ( ( R e. Top /\ S e. Top ) -> ran ( x e. ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |-> ( x i^i ( R Cn S ) ) ) C_ ( S ^ko R ) )
148 64 147 eqsstrd 
 |-  ( ( R e. Top /\ S e. Top ) -> ( ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |`t ( R Cn S ) ) C_ ( S ^ko R ) )
149 tgfiss 
 |-  ( ( ( S ^ko R ) e. Top /\ ( ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |`t ( R Cn S ) ) C_ ( S ^ko R ) ) -> ( topGen ` ( fi ` ( ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |`t ( R Cn S ) ) ) ) C_ ( S ^ko R ) )
150 55 148 149 syl2anc 
 |-  ( ( R e. Top /\ S e. Top ) -> ( topGen ` ( fi ` ( ( { ( U. S ^m X ) } u. ran ( k e. X , u e. S |-> ( `' ( w e. ( U. S ^m X ) |-> ( w ` k ) ) " u ) ) ) |`t ( R Cn S ) ) ) ) C_ ( S ^ko R ) )
151 54 150 eqsstrd 
 |-  ( ( R e. Top /\ S e. Top ) -> ( J |`t ( R Cn S ) ) C_ ( S ^ko R ) )