Metamath Proof Explorer


Theorem xkopt

Description: The compact-open topology on a discrete set coincides with the product topology where all the factors are the same. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion xkopt RTopAVR^ko𝒫A=𝑡A×R

Proof

Step Hyp Ref Expression
1 distop AV𝒫ATop
2 simpl RTopAVRTop
3 unipw 𝒫A=A
4 3 eqcomi A=𝒫A
5 eqid x𝒫A|𝒫A𝑡xComp=x𝒫A|𝒫A𝑡xComp
6 eqid kx𝒫A|𝒫A𝑡xComp,vRf𝒫ACnR|fkv=kx𝒫A|𝒫A𝑡xComp,vRf𝒫ACnR|fkv
7 4 5 6 xkoval 𝒫ATopRTopR^ko𝒫A=topGenfirankx𝒫A|𝒫A𝑡xComp,vRf𝒫ACnR|fkv
8 1 2 7 syl2an2 RTopAVR^ko𝒫A=topGenfirankx𝒫A|𝒫A𝑡xComp,vRf𝒫ACnR|fkv
9 simpr RTopAVAV
10 fconst6g RTopA×R:ATop
11 10 adantr RTopAVA×R:ATop
12 pttop AVA×R:ATop𝑡A×RTop
13 9 11 12 syl2anc RTopAV𝑡A×RTop
14 elpwi x𝒫AxA
15 restdis AVxA𝒫A𝑡x=𝒫x
16 14 15 sylan2 AVx𝒫A𝒫A𝑡x=𝒫x
17 16 adantll RTopAVx𝒫A𝒫A𝑡x=𝒫x
18 17 eleq1d RTopAVx𝒫A𝒫A𝑡xComp𝒫xComp
19 discmp xFin𝒫xComp
20 18 19 bitr4di RTopAVx𝒫A𝒫A𝑡xCompxFin
21 20 rabbidva RTopAVx𝒫A|𝒫A𝑡xComp=x𝒫A|xFin
22 dfin5 𝒫AFin=x𝒫A|xFin
23 21 22 eqtr4di RTopAVx𝒫A|𝒫A𝑡xComp=𝒫AFin
24 eqidd RTopAVR=R
25 toptopon2 RTopRTopOnR
26 cndis AVRTopOnR𝒫ACnR=RA
27 26 ancoms RTopOnRAV𝒫ACnR=RA
28 25 27 sylanb RTopAV𝒫ACnR=RA
29 28 rabeqdv RTopAVf𝒫ACnR|fkv=fRA|fkv
30 23 24 29 mpoeq123dv RTopAVkx𝒫A|𝒫A𝑡xComp,vRf𝒫ACnR|fkv=k𝒫AFin,vRfRA|fkv
31 30 rneqd RTopAVrankx𝒫A|𝒫A𝑡xComp,vRf𝒫ACnR|fkv=rank𝒫AFin,vRfRA|fkv
32 eqid k𝒫AFin,vRfRA|fkv=k𝒫AFin,vRfRA|fkv
33 32 rnmpo rank𝒫AFin,vRfRA|fkv=x|k𝒫AFinvRx=fRA|fkv
34 31 33 eqtrdi RTopAVrankx𝒫A|𝒫A𝑡xComp,vRf𝒫ACnR|fkv=x|k𝒫AFinvRx=fRA|fkv
35 elmapi fRAf:AR
36 eleq2 v=ifxkvRfxvfxifxkvR
37 36 imbi2d v=ifxkvRxAfxvxAfxifxkvR
38 37 bibi1d v=ifxkvRxAfxvxkfxvxAfxifxkvRxkfxv
39 eleq2 R=ifxkvRfxRfxifxkvR
40 39 imbi2d R=ifxkvRxAfxRxAfxifxkvR
41 40 bibi1d R=ifxkvRxAfxRxkfxvxAfxifxkvRxkfxv
42 simprl RTopAVk𝒫AFinvRk𝒫AFin
43 42 elin1d RTopAVk𝒫AFinvRk𝒫A
44 43 elpwid RTopAVk𝒫AFinvRkA
45 44 adantr RTopAVk𝒫AFinvRf:ARkA
46 45 sselda RTopAVk𝒫AFinvRf:ARxkxA
47 simpr RTopAVk𝒫AFinvRf:ARxkxk
48 46 47 2thd RTopAVk𝒫AFinvRf:ARxkxAxk
49 48 imbi1d RTopAVk𝒫AFinvRf:ARxkxAfxvxkfxv
50 ffvelcdm f:ARxAfxR
51 50 ex f:ARxAfxR
52 51 adantl RTopAVk𝒫AFinvRf:ARxAfxR
53 52 adantr RTopAVk𝒫AFinvRf:AR¬xkxAfxR
54 pm2.21 ¬xkxkfxv
55 54 adantl RTopAVk𝒫AFinvRf:AR¬xkxkfxv
56 53 55 2thd RTopAVk𝒫AFinvRf:AR¬xkxAfxRxkfxv
57 38 41 49 56 ifbothda RTopAVk𝒫AFinvRf:ARxAfxifxkvRxkfxv
58 57 ralbidv2 RTopAVk𝒫AFinvRf:ARxAfxifxkvRxkfxv
59 ffn f:ARfFnA
60 59 adantl RTopAVk𝒫AFinvRf:ARfFnA
61 vex fV
62 61 elixp fxAifxkvRfFnAxAfxifxkvR
63 62 baib fFnAfxAifxkvRxAfxifxkvR
64 60 63 syl RTopAVk𝒫AFinvRf:ARfxAifxkvRxAfxifxkvR
65 ffun f:ARFunf
66 fdm f:ARdomf=A
67 66 adantl RTopAVk𝒫AFinvRf:ARdomf=A
68 45 67 sseqtrrd RTopAVk𝒫AFinvRf:ARkdomf
69 funimass4 Funfkdomffkvxkfxv
70 65 68 69 syl2an2 RTopAVk𝒫AFinvRf:ARfkvxkfxv
71 58 64 70 3bitr4d RTopAVk𝒫AFinvRf:ARfxAifxkvRfkv
72 35 71 sylan2 RTopAVk𝒫AFinvRfRAfxAifxkvRfkv
73 72 rabbi2dva RTopAVk𝒫AFinvRRAxAifxkvR=fRA|fkv
74 elssuni vRvR
75 74 ad2antll RTopAVk𝒫AFinvRvR
76 ssid RR
77 sseq1 v=ifxkvRvRifxkvRR
78 sseq1 R=ifxkvRRRifxkvRR
79 77 78 ifboth vRRRifxkvRR
80 75 76 79 sylancl RTopAVk𝒫AFinvRifxkvRR
81 80 ralrimivw RTopAVk𝒫AFinvRxAifxkvRR
82 ss2ixp xAifxkvRRxAifxkvRxAR
83 81 82 syl RTopAVk𝒫AFinvRxAifxkvRxAR
84 simplr RTopAVk𝒫AFinvRAV
85 uniexg RTopRV
86 85 ad2antrr RTopAVk𝒫AFinvRRV
87 ixpconstg AVRVxAR=RA
88 84 86 87 syl2anc RTopAVk𝒫AFinvRxAR=RA
89 83 88 sseqtrd RTopAVk𝒫AFinvRxAifxkvRRA
90 sseqin2 xAifxkvRRARAxAifxkvR=xAifxkvR
91 89 90 sylib RTopAVk𝒫AFinvRRAxAifxkvR=xAifxkvR
92 73 91 eqtr3d RTopAVk𝒫AFinvRfRA|fkv=xAifxkvR
93 10 ad2antrr RTopAVk𝒫AFinvRA×R:ATop
94 42 elin2d RTopAVk𝒫AFinvRkFin
95 simplrr RTopAVk𝒫AFinvRxAvR
96 eqid R=R
97 96 topopn RTopRR
98 97 ad3antrrr RTopAVk𝒫AFinvRxARR
99 95 98 ifcld RTopAVk𝒫AFinvRxAifxkvRR
100 fvconst2g RTopxAA×Rx=R
101 100 ad4ant14 RTopAVk𝒫AFinvRxAA×Rx=R
102 99 101 eleqtrrd RTopAVk𝒫AFinvRxAifxkvRA×Rx
103 eldifn xAk¬xk
104 103 iffalsed xAkifxkvR=R
105 104 adantl RTopAVk𝒫AFinvRxAkifxkvR=R
106 eldifi xAkxA
107 106 101 sylan2 RTopAVk𝒫AFinvRxAkA×Rx=R
108 107 unieqd RTopAVk𝒫AFinvRxAkA×Rx=R
109 105 108 eqtr4d RTopAVk𝒫AFinvRxAkifxkvR=A×Rx
110 84 93 94 102 109 ptopn RTopAVk𝒫AFinvRxAifxkvR𝑡A×R
111 92 110 eqeltrd RTopAVk𝒫AFinvRfRA|fkv𝑡A×R
112 eleq1 x=fRA|fkvx𝑡A×RfRA|fkv𝑡A×R
113 111 112 syl5ibrcom RTopAVk𝒫AFinvRx=fRA|fkvx𝑡A×R
114 113 rexlimdvva RTopAVk𝒫AFinvRx=fRA|fkvx𝑡A×R
115 114 abssdv RTopAVx|k𝒫AFinvRx=fRA|fkv𝑡A×R
116 34 115 eqsstrd RTopAVrankx𝒫A|𝒫A𝑡xComp,vRf𝒫ACnR|fkv𝑡A×R
117 tgfiss 𝑡A×RToprankx𝒫A|𝒫A𝑡xComp,vRf𝒫ACnR|fkv𝑡A×RtopGenfirankx𝒫A|𝒫A𝑡xComp,vRf𝒫ACnR|fkv𝑡A×R
118 13 116 117 syl2anc RTopAVtopGenfirankx𝒫A|𝒫A𝑡xComp,vRf𝒫ACnR|fkv𝑡A×R
119 8 118 eqsstrd RTopAVR^ko𝒫A𝑡A×R
120 eqid 𝑡A×R=𝑡A×R
121 120 96 ptuniconst AVRTopRA=𝑡A×R
122 121 ancoms RTopAVRA=𝑡A×R
123 28 122 eqtrd RTopAV𝒫ACnR=𝑡A×R
124 123 oveq2d RTopAV𝑡A×R𝑡𝒫ACnR=𝑡A×R𝑡𝑡A×R
125 eqid 𝑡A×R=𝑡A×R
126 125 restid 𝑡A×RTop𝑡A×R𝑡𝑡A×R=𝑡A×R
127 13 126 syl RTopAV𝑡A×R𝑡𝑡A×R=𝑡A×R
128 124 127 eqtrd RTopAV𝑡A×R𝑡𝒫ACnR=𝑡A×R
129 4 120 xkoptsub 𝒫ATopRTop𝑡A×R𝑡𝒫ACnRR^ko𝒫A
130 1 2 129 syl2an2 RTopAV𝑡A×R𝑡𝒫ACnRR^ko𝒫A
131 128 130 eqsstrrd RTopAV𝑡A×RR^ko𝒫A
132 119 131 eqssd RTopAVR^ko𝒫A=𝑡A×R