Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkohmeo Structured version   Unicode version

Theorem xkohmeo 20767
 Description: The Exponential Law for topological spaces. The "currying" function is a homeomorphism on function spaces when and are exponentiable spaces (by xkococn 20612, it is sufficient to assume that are locally compact to ensure exponentiability). (Contributed by Mario Carneiro, 13-Apr-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
Hypotheses
Ref Expression
xkohmeo.x TopOn
xkohmeo.y TopOn
xkohmeo.f
xkohmeo.j 𝑛Locally
xkohmeo.k 𝑛Locally
xkohmeo.l
Assertion
Ref Expression
xkohmeo
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,

Proof of Theorem xkohmeo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xkohmeo.f . . 3
2 xkohmeo.x . . . . . . 7 TopOn
3 xkohmeo.y . . . . . . 7 TopOn
4 txtopon 20543 . . . . . . 7 TopOn TopOn TopOn
52, 3, 4syl2anc 665 . . . . . 6 TopOn
6 topontop 19878 . . . . . 6 TopOn
75, 6syl 17 . . . . 5
8 xkohmeo.l . . . . 5
9 eqid 2420 . . . . . 6
109xkotopon 20552 . . . . 5 TopOn
117, 8, 10syl2anc 665 . . . 4 TopOn
12 vex 3081 . . . . . . . . 9
13 vex 3081 . . . . . . . . 9
1412, 13op1std 6808 . . . . . . . 8
1512, 13op2ndd 6809 . . . . . . . 8
16 eqidd 2421 . . . . . . . 8
1714, 15, 16oveq123d 6317 . . . . . . 7
1817mpteq2dv 4504 . . . . . 6
1918mpt2mpt 6393 . . . . 5
20 txtopon 20543 . . . . . . 7 TopOn TopOn TopOn
2111, 2, 20syl2anc 665 . . . . . 6 TopOn
22 vex 3081 . . . . . . . . . . 11
23 vex 3081 . . . . . . . . . . 11
2422, 23op1std 6808 . . . . . . . . . 10
2524fveq2d 5876 . . . . . . . . 9
2624fveq2d 5876 . . . . . . . . 9
2722, 23op2ndd 6809 . . . . . . . . 9
2825, 26, 27oveq123d 6317 . . . . . . . 8
2928mpt2mpt 6393 . . . . . . 7
30 txtopon 20543 . . . . . . . . 9 TopOn TopOn TopOn
3121, 3, 30syl2anc 665 . . . . . . . 8 TopOn
32 eqid 2420 . . . . . . . . . 10
3332toptopon 19885 . . . . . . . . 9 TopOn
348, 33sylib 199 . . . . . . . 8 TopOn
35 xkohmeo.j . . . . . . . . 9 𝑛Locally
36 xkohmeo.k . . . . . . . . 9 𝑛Locally
37 txcmp 20595 . . . . . . . . . 10
3837txnlly 20589 . . . . . . . . 9 𝑛Locally 𝑛Locally 𝑛Locally
3935, 36, 38syl2anc 665 . . . . . . . 8 𝑛Locally
4025mpt2mpt 6393 . . . . . . . . . 10
415adantr 466 . . . . . . . . . . . . 13 TopOn
4234adantr 466 . . . . . . . . . . . . 13 TopOn
43 xp1st 6828 . . . . . . . . . . . . . . 15
4443adantl 467 . . . . . . . . . . . . . 14
45 xp1st 6828 . . . . . . . . . . . . . 14
4644, 45syl 17 . . . . . . . . . . . . 13
47 cnf2 20202 . . . . . . . . . . . . 13 TopOn TopOn
4841, 42, 46, 47syl3anc 1264 . . . . . . . . . . . 12
4948feqmptd 5925 . . . . . . . . . . 11
5049mpteq2dva 4503 . . . . . . . . . 10
5140, 50syl5eqr 2475 . . . . . . . . 9
5221, 3cnmpt1st 20620 . . . . . . . . . 10
53 fveq2 5872 . . . . . . . . . . . 12
5453cbvmptv 4509 . . . . . . . . . . 11
5514mpt2mpt 6393 . . . . . . . . . . . 12
5611, 2cnmpt1st 20620 . . . . . . . . . . . 12
5755, 56syl5eqel 2512 . . . . . . . . . . 11
5854, 57syl5eqel 2512 . . . . . . . . . 10
5921, 3, 52, 21, 58, 53cnmpt21 20623 . . . . . . . . 9
6051, 59eqeltrrd 2509 . . . . . . . 8
6126mpt2mpt 6393 . . . . . . . . . 10
62 fveq2 5872 . . . . . . . . . . . . 13
6362cbvmptv 4509 . . . . . . . . . . . 12
6415mpt2mpt 6393 . . . . . . . . . . . . 13
6511, 2cnmpt2nd 20621 . . . . . . . . . . . . 13
6664, 65syl5eqel 2512 . . . . . . . . . . . 12
6763, 66syl5eqel 2512 . . . . . . . . . . 11
6821, 3, 52, 21, 67, 62cnmpt21 20623 . . . . . . . . . 10
6961, 68syl5eqel 2512 . . . . . . . . 9
7027mpt2mpt 6393 . . . . . . . . . 10
7121, 3cnmpt2nd 20621 . . . . . . . . . 10
7270, 71syl5eqel 2512 . . . . . . . . 9
7331, 69, 72cnmpt1t 20617 . . . . . . . 8
74 fveq2 5872 . . . . . . . . 9
75 df-ov 6299 . . . . . . . . 9
7674, 75syl6eqr 2479 . . . . . . . 8
7731, 5, 34, 39, 60, 73, 76cnmptk1p 20637 . . . . . . 7
7829, 77syl5eqelr 2513 . . . . . 6
7921, 3, 78cnmpt2k 20640 . . . . 5
8019, 79syl5eqelr 2513 . . . 4
8111, 2, 80cnmpt2k 20640 . . 3
821, 81syl5eqel 2512 . 2
832, 3, 1, 35, 36, 8xkocnv 20766 . . . 4
8413, 23op1std 6808 . . . . . . . 8
8584fveq2d 5876 . . . . . . 7
8613, 23op2ndd 6809 . . . . . . 7
8785, 86fveq12d 5878 . . . . . 6
8887mpt2mpt 6393 . . . . 5
8988mpteq2i 4500 . . . 4
9083, 89syl6eqr 2479 . . 3
91 nllytop 20425 . . . . . 6 𝑛Locally
9235, 91syl 17 . . . . 5
93 nllytop 20425 . . . . . . 7 𝑛Locally
9436, 93syl 17 . . . . . 6
95 xkotop 20540 . . . . . 6
9694, 8, 95syl2anc 665 . . . . 5
97 eqid 2420 . . . . . 6
9897xkotopon 20552 . . . . 5 TopOn
9992, 96, 98syl2anc 665 . . . 4 TopOn
100 vex 3081 . . . . . . . . 9
101100, 22op1std 6808 . . . . . . . 8
102100, 22op2ndd 6809 . . . . . . . . 9
103102fveq2d 5876 . . . . . . . 8
104101, 103fveq12d 5878 . . . . . . 7
105102fveq2d 5876 . . . . . . 7
106104, 105fveq12d 5878 . . . . . 6
107106mpt2mpt 6393 . . . . 5
108 txtopon 20543 . . . . . . 7 TopOn TopOn TopOn
10999, 5, 108syl2anc 665 . . . . . 6 TopOn
1103adantr 466 . . . . . . . . . 10 TopOn
11134adantr 466 . . . . . . . . . 10 TopOn
1122adantr 466 . . . . . . . . . . . 12 TopOn
113 eqid 2420 . . . . . . . . . . . . . . 15
114113xkotopon 20552 . . . . . . . . . . . . . 14 TopOn
11594, 8, 114syl2anc 665 . . . . . . . . . . . . 13 TopOn
116115adantr 466 . . . . . . . . . . . 12 TopOn
117 xp1st 6828 . . . . . . . . . . . . 13
118117adantl 467 . . . . . . . . . . . 12
119 cnf2 20202 . . . . . . . . . . . 12 TopOn TopOn
120112, 116, 118, 119syl3anc 1264 . . . . . . . . . . 11
121 xp2nd 6829 . . . . . . . . . . . . 13
122121adantl 467 . . . . . . . . . . . 12
123 xp1st 6828 . . . . . . . . . . . 12
124122, 123syl 17 . . . . . . . . . . 11
125120, 124ffvelrnd 6029 . . . . . . . . . 10
126 cnf2 20202 . . . . . . . . . 10 TopOn TopOn
127110, 111, 125, 126syl3anc 1264 . . . . . . . . 9
128127feqmptd 5925 . . . . . . . 8
129128mpteq2dva 4503 . . . . . . 7
130101mpt2mpt 6393 . . . . . . . . . 10
131120feqmptd 5925 . . . . . . . . . . 11
132131mpteq2dva 4503 . . . . . . . . . 10
133130, 132syl5eqr 2475 . . . . . . . . 9
13499, 5cnmpt1st 20620 . . . . . . . . 9
135133, 134eqeltrrd 2509 . . . . . . . 8
136103mpt2mpt 6393 . . . . . . . . 9
13799, 5cnmpt2nd 20621 . . . . . . . . . 10
13853cbvmptv 4509 . . . . . . . . . . 11
13984mpt2mpt 6393 . . . . . . . . . . . 12
1402, 3cnmpt1st 20620 . . . . . . . . . . . 12
141139, 140syl5eqel 2512 . . . . . . . . . . 11
142138, 141syl5eqel 2512 . . . . . . . . . 10
14399, 5, 137, 5, 142, 53cnmpt21 20623 . . . . . . . . 9
144136, 143syl5eqel 2512 . . . . . . . 8
145 fveq2 5872 . . . . . . . 8
146109, 2, 115, 35, 135, 144, 145cnmptk1p 20637 . . . . . . 7
147129, 146eqeltrrd 2509 . . . . . 6
148105mpt2mpt 6393 . . . . . . 7
14962cbvmptv 4509 . . . . . . . . 9
15086mpt2mpt 6393 . . . . . . . . . 10
1512, 3cnmpt2nd 20621 . . . . . . . . . 10
152150, 151syl5eqel 2512 . . . . . . . . 9
153149, 152syl5eqel 2512 . . . . . . . 8
15499, 5, 137, 5, 153, 62cnmpt21 20623 . . . . . . 7
155148, 154syl5eqel 2512 . . . . . 6
156 fveq2 5872 . . . . . 6
157109, 3, 34, 36, 147, 155, 156cnmptk1p 20637 . . . . 5
158107, 157syl5eqelr 2513 . . . 4
15999, 5, 158cnmpt2k 20640 . . 3
16090, 159eqeltrd 2508 . 2
161 ishmeo 20711 . 2
16282, 160, 161sylanbrc 668 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   wceq 1437   wcel 1867  cop 3999  cuni 4213   cmpt 4475   cxp 4843  ccnv 4844  wf 5588  cfv 5592  (class class class)co 6296   cmpt2 6298  c1st 6796  c2nd 6797  ctop 19854  TopOnctopon 19855   ccn 20177  ccmp 20338  𝑛Locally cnlly 20417   ctx 20512   cxko 20513  chmeo 20705 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4529  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-iin 4296  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-1o 7181  df-2o 7182  df-oadd 7185  df-er 7362  df-map 7473  df-ixp 7522  df-en 7569  df-dom 7570  df-sdom 7571  df-fin 7572  df-fi 7922  df-rest 15281  df-topgen 15302  df-pt 15303  df-top 19858  df-bases 19859  df-topon 19860  df-ntr 19972  df-nei 20051  df-cn 20180  df-cnp 20181  df-cmp 20339  df-nlly 20419  df-tx 20514  df-xko 20515  df-hmeo 20707 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator