Metamath Proof Explorer

Theorem kgencn3

Description: The set of continuous functions from J to K is unaffected by k-ification of K , if J is already compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion kgencn3 
|- ( ( J e. ran kGen /\ K e. Top ) -> ( J Cn K ) = ( J Cn ( kGen ` K ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 eqid 
 |-  U. K = U. K
3 1 2 cnf 
 |-  ( f e. ( J Cn K ) -> f : U. J --> U. K )
4 3 adantl 
 |-  ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> f : U. J --> U. K )
5 cnvimass 
 |-  ( `' f " x ) C_ dom f
6 4 fdmd 
 |-  ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> dom f = U. J )
7 6 adantr 
 |-  ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> dom f = U. J )
8 5 7 sseqtrid 
 |-  ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> ( `' f " x ) C_ U. J )
9 cnvresima 
 |-  ( `' ( f |` y ) " ( x i^i ( f " y ) ) ) = ( ( `' f " ( x i^i ( f " y ) ) ) i^i y )
10 4 ad2antrr 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> f : U. J --> U. K )
11 ffun 
 |-  ( f : U. J --> U. K -> Fun f )
12 inpreima 
 |-  ( Fun f -> ( `' f " ( x i^i ( f " y ) ) ) = ( ( `' f " x ) i^i ( `' f " ( f " y ) ) ) )
13 10 11 12 3syl 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( `' f " ( x i^i ( f " y ) ) ) = ( ( `' f " x ) i^i ( `' f " ( f " y ) ) ) )
14 13 ineq1d 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( `' f " ( x i^i ( f " y ) ) ) i^i y ) = ( ( ( `' f " x ) i^i ( `' f " ( f " y ) ) ) i^i y ) )
15 in32 
 |-  ( ( ( `' f " x ) i^i ( `' f " ( f " y ) ) ) i^i y ) = ( ( ( `' f " x ) i^i y ) i^i ( `' f " ( f " y ) ) )
16 ssrin 
 |-  ( ( `' f " x ) C_ dom f -> ( ( `' f " x ) i^i y ) C_ ( dom f i^i y ) )
17 5 16 ax-mp 
 |-  ( ( `' f " x ) i^i y ) C_ ( dom f i^i y )
18 dminss 
 |-  ( dom f i^i y ) C_ ( `' f " ( f " y ) )
19 17 18 sstri 
 |-  ( ( `' f " x ) i^i y ) C_ ( `' f " ( f " y ) )
20 19 a1i 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( `' f " x ) i^i y ) C_ ( `' f " ( f " y ) ) )
21 df-ss 
 |-  ( ( ( `' f " x ) i^i y ) C_ ( `' f " ( f " y ) ) <-> ( ( ( `' f " x ) i^i y ) i^i ( `' f " ( f " y ) ) ) = ( ( `' f " x ) i^i y ) )
22 20 21 sylib 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( ( `' f " x ) i^i y ) i^i ( `' f " ( f " y ) ) ) = ( ( `' f " x ) i^i y ) )
23 15 22 syl5eq 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( ( `' f " x ) i^i ( `' f " ( f " y ) ) ) i^i y ) = ( ( `' f " x ) i^i y ) )
24 14 23 eqtrd 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( `' f " ( x i^i ( f " y ) ) ) i^i y ) = ( ( `' f " x ) i^i y ) )
25 9 24 syl5eq 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( `' ( f |` y ) " ( x i^i ( f " y ) ) ) = ( ( `' f " x ) i^i y ) )
26 simpr 
 |-  ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> f e. ( J Cn K ) )
27 26 ad2antrr 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> f e. ( J Cn K ) )
28 elpwi 
 |-  ( y e. ~P U. J -> y C_ U. J )
29 28 ad2antrl 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> y C_ U. J )
30 1 cnrest 
 |-  ( ( f e. ( J Cn K ) /\ y C_ U. J ) -> ( f |` y ) e. ( ( J |`t y ) Cn K ) )
31 27 29 30 syl2anc 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( f |` y ) e. ( ( J |`t y ) Cn K ) )
32 simpr 
 |-  ( ( J e. ran kGen /\ K e. Top ) -> K e. Top )
33 32 ad3antrrr 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> K e. Top )
34 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
35 33 34 sylib 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> K e. ( TopOn ` U. K ) )
36 df-ima 
 |-  ( f " y ) = ran ( f |` y )
37 36 eqimss2i 
 |-  ran ( f |` y ) C_ ( f " y )
38 37 a1i 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ran ( f |` y ) C_ ( f " y ) )
39 imassrn 
 |-  ( f " y ) C_ ran f
40 10 frnd 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ran f C_ U. K )
41 39 40 sstrid 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( f " y ) C_ U. K )
42 cnrest2 
 |-  ( ( K e. ( TopOn ` U. K ) /\ ran ( f |` y ) C_ ( f " y ) /\ ( f " y ) C_ U. K ) -> ( ( f |` y ) e. ( ( J |`t y ) Cn K ) <-> ( f |` y ) e. ( ( J |`t y ) Cn ( K |`t ( f " y ) ) ) ) )
43 35 38 41 42 syl3anc 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( f |` y ) e. ( ( J |`t y ) Cn K ) <-> ( f |` y ) e. ( ( J |`t y ) Cn ( K |`t ( f " y ) ) ) ) )
44 31 43 mpbid 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( f |` y ) e. ( ( J |`t y ) Cn ( K |`t ( f " y ) ) ) )
45 simplr 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> x e. ( kGen ` K ) )
46 simprr 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( J |`t y ) e. Comp )
47 imacmp 
 |-  ( ( f e. ( J Cn K ) /\ ( J |`t y ) e. Comp ) -> ( K |`t ( f " y ) ) e. Comp )
48 27 46 47 syl2anc 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( K |`t ( f " y ) ) e. Comp )
49 kgeni 
 |-  ( ( x e. ( kGen ` K ) /\ ( K |`t ( f " y ) ) e. Comp ) -> ( x i^i ( f " y ) ) e. ( K |`t ( f " y ) ) )
50 45 48 49 syl2anc 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( x i^i ( f " y ) ) e. ( K |`t ( f " y ) ) )
51 cnima 
 |-  ( ( ( f |` y ) e. ( ( J |`t y ) Cn ( K |`t ( f " y ) ) ) /\ ( x i^i ( f " y ) ) e. ( K |`t ( f " y ) ) ) -> ( `' ( f |` y ) " ( x i^i ( f " y ) ) ) e. ( J |`t y ) )
52 44 50 51 syl2anc 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( `' ( f |` y ) " ( x i^i ( f " y ) ) ) e. ( J |`t y ) )
53 25 52 eqeltrrd 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( `' f " x ) i^i y ) e. ( J |`t y ) )
54 53 expr 
 |-  ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ y e. ~P U. J ) -> ( ( J |`t y ) e. Comp -> ( ( `' f " x ) i^i y ) e. ( J |`t y ) ) )
55 54 ralrimiva 
 |-  ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> A. y e. ~P U. J ( ( J |`t y ) e. Comp -> ( ( `' f " x ) i^i y ) e. ( J |`t y ) ) )
56 kgentop 
 |-  ( J e. ran kGen -> J e. Top )
57 56 ad3antrrr 
 |-  ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> J e. Top )
58 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
59 57 58 sylib 
 |-  ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> J e. ( TopOn ` U. J ) )
60 elkgen 
 |-  ( J e. ( TopOn ` U. J ) -> ( ( `' f " x ) e. ( kGen ` J ) <-> ( ( `' f " x ) C_ U. J /\ A. y e. ~P U. J ( ( J |`t y ) e. Comp -> ( ( `' f " x ) i^i y ) e. ( J |`t y ) ) ) ) )
61 59 60 syl 
 |-  ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> ( ( `' f " x ) e. ( kGen ` J ) <-> ( ( `' f " x ) C_ U. J /\ A. y e. ~P U. J ( ( J |`t y ) e. Comp -> ( ( `' f " x ) i^i y ) e. ( J |`t y ) ) ) ) )
62 8 55 61 mpbir2and 
 |-  ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> ( `' f " x ) e. ( kGen ` J ) )
63 kgenidm 
 |-  ( J e. ran kGen -> ( kGen ` J ) = J )
64 63 ad3antrrr 
 |-  ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> ( kGen ` J ) = J )
65 62 64 eleqtrd 
 |-  ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> ( `' f " x ) e. J )
66 65 ralrimiva 
 |-  ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> A. x e. ( kGen ` K ) ( `' f " x ) e. J )
67 56 58 sylib 
 |-  ( J e. ran kGen -> J e. ( TopOn ` U. J ) )
68 kgentopon 
 |-  ( K e. ( TopOn ` U. K ) -> ( kGen ` K ) e. ( TopOn ` U. K ) )
69 34 68 sylbi 
 |-  ( K e. Top -> ( kGen ` K ) e. ( TopOn ` U. K ) )
70 iscn 
 |-  ( ( J e. ( TopOn ` U. J ) /\ ( kGen ` K ) e. ( TopOn ` U. K ) ) -> ( f e. ( J Cn ( kGen ` K ) ) <-> ( f : U. J --> U. K /\ A. x e. ( kGen ` K ) ( `' f " x ) e. J ) ) )
71 67 69 70 syl2an 
 |-  ( ( J e. ran kGen /\ K e. Top ) -> ( f e. ( J Cn ( kGen ` K ) ) <-> ( f : U. J --> U. K /\ A. x e. ( kGen ` K ) ( `' f " x ) e. J ) ) )
72 71 adantr 
 |-  ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> ( f e. ( J Cn ( kGen ` K ) ) <-> ( f : U. J --> U. K /\ A. x e. ( kGen ` K ) ( `' f " x ) e. J ) ) )
73 4 66 72 mpbir2and 
 |-  ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> f e. ( J Cn ( kGen ` K ) ) )
74 73 ex 
 |-  ( ( J e. ran kGen /\ K e. Top ) -> ( f e. ( J Cn K ) -> f e. ( J Cn ( kGen ` K ) ) ) )
75 74 ssrdv 
 |-  ( ( J e. ran kGen /\ K e. Top ) -> ( J Cn K ) C_ ( J Cn ( kGen ` K ) ) )
76 69 adantl 
 |-  ( ( J e. ran kGen /\ K e. Top ) -> ( kGen ` K ) e. ( TopOn ` U. K ) )
77 toponcom 
 |-  ( ( K e. Top /\ ( kGen ` K ) e. ( TopOn ` U. K ) ) -> K e. ( TopOn ` U. ( kGen ` K ) ) )
78 32 76 77 syl2anc 
 |-  ( ( J e. ran kGen /\ K e. Top ) -> K e. ( TopOn ` U. ( kGen ` K ) ) )
79 kgenss 
 |-  ( K e. Top -> K C_ ( kGen ` K ) )
80 79 adantl 
 |-  ( ( J e. ran kGen /\ K e. Top ) -> K C_ ( kGen ` K ) )
81 eqid 
 |-  U. ( kGen ` K ) = U. ( kGen ` K )
82 81 cnss2 
 |-  ( ( K e. ( TopOn ` U. ( kGen ` K ) ) /\ K C_ ( kGen ` K ) ) -> ( J Cn ( kGen ` K ) ) C_ ( J Cn K ) )
83 78 80 82 syl2anc 
 |-  ( ( J e. ran kGen /\ K e. Top ) -> ( J Cn ( kGen ` K ) ) C_ ( J Cn K ) )
84 75 83 eqssd 
 |-  ( ( J e. ran kGen /\ K e. Top ) -> ( J Cn K ) = ( J Cn ( kGen ` K ) ) )