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

Theorem pt1hmeo 17839
 Description: The canonical homeomorphism from a topological product on a singleton to the topology of the factor. (Contributed by Mario Carneiro, 3-Feb-2015.)
Hypotheses
Ref Expression
pt1hmeo.j
pt1hmeo.a
pt1hmeo.r TopOn
Assertion
Ref Expression
pt1hmeo
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem pt1hmeo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fconstmpt 4922 . . . . 5
2 pt1hmeo.a . . . . . . 7
32adantr 453 . . . . . 6
4 sneq 3826 . . . . . . . . 9
54xpeq1d 4902 . . . . . . . 8
6 opeq1 3985 . . . . . . . . 9
76sneqd 3828 . . . . . . . 8
85, 7eqeq12d 2451 . . . . . . 7
9 vex 2960 . . . . . . . 8
10 vex 2960 . . . . . . . 8
119, 10xpsn 5911 . . . . . . 7
128, 11vtoclg 3012 . . . . . 6
133, 12syl 16 . . . . 5
141, 13syl5eqr 2483 . . . 4
1514mpteq2dva 4296 . . 3
16 pt1hmeo.j . . . 4
17 pt1hmeo.r . . . 4 TopOn
18 snex 4406 . . . . 5
1918a1i 11 . . . 4
20 f1osng 5717 . . . . . . 7 TopOn
212, 17, 20syl2anc 644 . . . . . 6
22 f1of 5675 . . . . . 6
2321, 22syl 16 . . . . 5
24 topontop 16992 . . . . . . 7 TopOn
2517, 24syl 16 . . . . . 6
2625snssd 3944 . . . . 5
27 fss 5600 . . . . 5
2823, 26, 27syl2anc 644 . . . 4
2917cnmptid 17694 . . . . . 6
3029adantr 453 . . . . 5
31 elsni 3839 . . . . . . . 8
3231fveq2d 5733 . . . . . . 7
33 fvsng 5928 . . . . . . . 8 TopOn
342, 17, 33syl2anc 644 . . . . . . 7
3532, 34sylan9eqr 2491 . . . . . 6
3635oveq2d 6098 . . . . 5
3730, 36eleqtrrd 2514 . . . 4
3816, 17, 19, 28, 37ptcn 17660 . . 3
3915, 38eqeltrrd 2512 . 2
40 simprr 735 . . . . . . . . . 10
4114adantrr 699 . . . . . . . . . 10
4240, 41eqtr4d 2472 . . . . . . . . 9
43 simprl 734 . . . . . . . . . . . 12
4443adantr 453 . . . . . . . . . . 11
45 eqid 2437 . . . . . . . . . . 11
4644, 45fmptd 5894 . . . . . . . . . 10
47 toponmax 16994 . . . . . . . . . . . . 13 TopOn
4817, 47syl 16 . . . . . . . . . . . 12
4948adantr 453 . . . . . . . . . . 11
50 elmapg 7032 . . . . . . . . . . 11
5149, 18, 50sylancl 645 . . . . . . . . . 10
5246, 51mpbird 225 . . . . . . . . 9
5342, 52eqeltrd 2511 . . . . . . . 8
5440fveq1d 5731 . . . . . . . . 9
552adantr 453 . . . . . . . . . 10
56 fvsng 5928 . . . . . . . . . 10
5755, 43, 56syl2anc 644 . . . . . . . . 9
5854, 57eqtr2d 2470 . . . . . . . 8
5953, 58jca 520 . . . . . . 7
60 simprr 735 . . . . . . . . 9
61 simprl 734 . . . . . . . . . . 11
6248adantr 453 . . . . . . . . . . . 12
63 elmapg 7032 . . . . . . . . . . . 12
6462, 18, 63sylancl 645 . . . . . . . . . . 11
6561, 64mpbid 203 . . . . . . . . . 10
66 snidg 3840 . . . . . . . . . . . 12
672, 66syl 16 . . . . . . . . . . 11
6867adantr 453 . . . . . . . . . 10
6965, 68ffvelrnd 5872 . . . . . . . . 9
7060, 69eqeltrd 2511 . . . . . . . 8
712adantr 453 . . . . . . . . . . . 12
724feq2d 5582 . . . . . . . . . . . . 13
73 fveq2 5729 . . . . . . . . . . . . . . 15
7473eleq1d 2503 . . . . . . . . . . . . . 14
75 id 21 . . . . . . . . . . . . . . . . 17
7675, 73opeq12d 3993 . . . . . . . . . . . . . . . 16
7776sneqd 3828 . . . . . . . . . . . . . . 15
7877eqeq2d 2448 . . . . . . . . . . . . . 14
7974, 78anbi12d 693 . . . . . . . . . . . . 13
809fsn2 5909 . . . . . . . . . . . . 13
8172, 79, 80vtoclbg 3013 . . . . . . . . . . . 12
8271, 81syl 16 . . . . . . . . . . 11
8365, 82mpbid 203 . . . . . . . . . 10
8483simprd 451 . . . . . . . . 9
8560opeq2d 3992 . . . . . . . . . 10
8685sneqd 3828 . . . . . . . . 9
8784, 86eqtr4d 2472 . . . . . . . 8
8870, 87jca 520 . . . . . . 7
8959, 88impbida 807 . . . . . 6
9089opabbidv 4272 . . . . 5
91 df-mpt 4269 . . . . . . 7
9291cnveqi 5048 . . . . . 6
93 cnvopab 5275 . . . . . 6
9492, 93eqtri 2457 . . . . 5
95 df-mpt 4269 . . . . 5
9690, 94, 953eqtr4g 2494 . . . 4
97 xpsng 5910 . . . . . . . . . . 11 TopOn
982, 17, 97syl2anc 644 . . . . . . . . . 10
9998eqcomd 2442 . . . . . . . . 9
10099fveq2d 5733 . . . . . . . 8
10116, 100syl5eq 2481 . . . . . . 7
102 eqid 2437 . . . . . . . . 9
103102pttoponconst 17630 . . . . . . . 8 TopOn TopOn
10419, 17, 103syl2anc 644 . . . . . . 7 TopOn
105101, 104eqeltrd 2511 . . . . . 6 TopOn
106 toponuni 16993 . . . . . 6 TopOn
107105, 106syl 16 . . . . 5
108107mpteq1d 4291 . . . 4
10996, 108eqtrd 2469 . . 3
110 eqid 2437 . . . . . 6
111110, 16ptpjcn 17644 . . . . 5
11219, 28, 67, 111syl3anc 1185 . . . 4
11334oveq2d 6098 . . . 4
114112, 113eleqtrd 2513 . . 3
115109, 114eqeltrd 2511 . 2
116 ishmeo 17792 . 2
11739, 115, 116sylanbrc 647 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   wceq 1653   wcel 1726  cvv 2957   wss 3321  csn 3815  cop 3818  cuni 4016  copab 4266   cmpt 4267   cxp 4877  ccnv 4878  wf 5451  wf1o 5454  cfv 5455  (class class class)co 6082   cmap 7019  cpt 13667  ctop 16959  TopOnctopon 16960   ccn 17289   chmeo 17786 This theorem is referenced by:  xpstopnlem1  17842  ptcmpfi  17846 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-rep 4321  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-reu 2713  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-int 4052  df-iun 4096  df-iin 4097  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-1st 6350  df-2nd 6351  df-recs 6634  df-rdg 6669  df-1o 6725  df-oadd 6729  df-er 6906  df-map 7021  df-ixp 7065  df-en 7111  df-dom 7112  df-fin 7114  df-fi 7417  df-topgen 13668  df-pt 13669  df-top 16964  df-bases 16966  df-topon 16967  df-cn 17292  df-cnp 17293  df-hmeo 17788
 Copyright terms: Public domain W3C validator