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

Theorem qtoprest 17408
 Description: If is a saturated open or closed set (where saturated means that for some ), then the restriction of the quotient map to is a quotient map. (Contributed by Mario Carneiro, 24-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
qtoprest.2 TopOn
qtoprest.3
qtoprest.4
qtoprest.5
qtoprest.6
Assertion
Ref Expression
qtoprest qTop t t qTop

Proof of Theorem qtoprest
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 qtoprest.2 . . . . . 6 TopOn
2 qtoprest.3 . . . . . . 7
3 fofn 5453 . . . . . . 7
42, 3syl 15 . . . . . 6
5 qtopid 17396 . . . . . 6 TopOn qTop
61, 4, 5syl2anc 642 . . . . 5 qTop
7 qtoprest.5 . . . . . . 7
8 cnvimass 5033 . . . . . . . 8
9 fndm 5343 . . . . . . . . 9
104, 9syl 15 . . . . . . . 8
118, 10syl5sseq 3226 . . . . . . 7
127, 11eqsstrd 3212 . . . . . 6
13 toponuni 16665 . . . . . . 7 TopOn
141, 13syl 15 . . . . . 6
1512, 14sseqtrd 3214 . . . . 5
16 eqid 2283 . . . . . 6
1716cnrest 17013 . . . . 5 qTop t qTop
186, 15, 17syl2anc 642 . . . 4 t qTop
19 qtoptopon 17395 . . . . . 6 TopOn qTop TopOn
201, 2, 19syl2anc 642 . . . . 5 qTop TopOn
21 df-ima 4702 . . . . . . 7
227imaeq2d 5012 . . . . . . . 8
23 qtoprest.4 . . . . . . . . 9
24 foimacnv 5490 . . . . . . . . 9
252, 23, 24syl2anc 642 . . . . . . . 8
2622, 25eqtrd 2315 . . . . . . 7
2721, 26syl5eqr 2329 . . . . . 6
28 eqimss 3230 . . . . . 6
2927, 28syl 15 . . . . 5
30 cnrest2 17014 . . . . 5 qTop TopOn t qTop t qTop t
3120, 29, 23, 30syl3anc 1182 . . . 4 t qTop t qTop t
3218, 31mpbid 201 . . 3 t qTop t
33 resttopon 16892 . . . 4 qTop TopOn qTop t TopOn
3420, 23, 33syl2anc 642 . . 3 qTop t TopOn
35 qtopss 17406 . . 3 t qTop t qTop t TopOn qTop t t qTop
3632, 34, 27, 35syl3anc 1182 . 2 qTop t t qTop
37 resttopon 16892 . . . . . 6 TopOn t TopOn
381, 12, 37syl2anc 642 . . . . 5 t TopOn
39 fnfun 5341 . . . . . . . 8
404, 39syl 15 . . . . . . 7
4112, 10sseqtr4d 3215 . . . . . . 7
42 fores 5460 . . . . . . 7
4340, 41, 42syl2anc 642 . . . . . 6
44 foeq3 5449 . . . . . . 7
4526, 44syl 15 . . . . . 6
4643, 45mpbid 201 . . . . 5
47 elqtop3 17394 . . . . 5 t TopOn t qTop t
4838, 46, 47syl2anc 642 . . . 4 t qTop t
49 cnvresima 5162 . . . . . . . 8
50 imass2 5049 . . . . . . . . . . 11
5150adantl 452 . . . . . . . . . 10
527adantr 451 . . . . . . . . . 10
5351, 52sseqtr4d 3215 . . . . . . . . 9
54 df-ss 3166 . . . . . . . . 9
5553, 54sylib 188 . . . . . . . 8
5649, 55syl5eq 2327 . . . . . . 7
5756eleq1d 2349 . . . . . 6 t t
58 simplrl 736 . . . . . . . . . 10 t
59 df-ss 3166 . . . . . . . . . 10
6058, 59sylib 188 . . . . . . . . 9 t
61 topontop 16664 . . . . . . . . . . . 12 qTop TopOn qTop
6220, 61syl 15 . . . . . . . . . . 11 qTop
6362ad2antrr 706 . . . . . . . . . 10 t qTop
64 toponmax 16666 . . . . . . . . . . . . . 14 TopOn
651, 64syl 15 . . . . . . . . . . . . 13
66 fornex 5750 . . . . . . . . . . . . 13
6765, 2, 66sylc 56 . . . . . . . . . . . 12
68 ssexg 4160 . . . . . . . . . . . 12
6923, 67, 68syl2anc 642 . . . . . . . . . . 11
7069ad2antrr 706 . . . . . . . . . 10 t
7123ad2antrr 706 . . . . . . . . . . . 12 t
7258, 71sstrd 3189 . . . . . . . . . . 11 t
73 topontop 16664 . . . . . . . . . . . . . . . 16 TopOn
741, 73syl 15 . . . . . . . . . . . . . . 15
75 restopn2 16908 . . . . . . . . . . . . . . 15 t
7674, 75sylan 457 . . . . . . . . . . . . . 14 t
7776simprbda 606 . . . . . . . . . . . . 13 t
7877adantrl 696 . . . . . . . . . . . 12 t
7978an32s 779 . . . . . . . . . . 11 t
80 elqtop3 17394 . . . . . . . . . . . . 13 TopOn qTop
811, 2, 80syl2anc 642 . . . . . . . . . . . 12 qTop
8281ad2antrr 706 . . . . . . . . . . 11 t qTop
8372, 79, 82mpbir2and 888 . . . . . . . . . 10 t qTop
84 elrestr 13333 . . . . . . . . . 10 qTop qTop qTop t
8563, 70, 83, 84syl3anc 1182 . . . . . . . . 9 t qTop t
8660, 85eqeltrrd 2358 . . . . . . . 8 t qTop t
8734ad2antrr 706 . . . . . . . . . . . 12 t qTop t TopOn
88 toponuni 16665 . . . . . . . . . . . 12 qTop t TopOn qTop t
8987, 88syl 15 . . . . . . . . . . 11 t qTop t
9089difeq1d 3293 . . . . . . . . . 10 t qTop t
9123ad2antrr 706 . . . . . . . . . . . 12 t
9220ad2antrr 706 . . . . . . . . . . . . 13 t qTop TopOn
93 toponuni 16665 . . . . . . . . . . . . 13 qTop TopOn qTop
9492, 93syl 15 . . . . . . . . . . . 12 t qTop
9591, 94sseqtrd 3214 . . . . . . . . . . 11 t qTop
96 difss 3303 . . . . . . . . . . . . 13
9796, 91syl5ss 3190 . . . . . . . . . . . 12 t
9840ad2antrr 706 . . . . . . . . . . . . . . 15 t
99 funcnvcnv 5308 . . . . . . . . . . . . . . 15
100 imadif 5327 . . . . . . . . . . . . . . 15
10198, 99, 1003syl 18 . . . . . . . . . . . . . 14 t
1027ad2antrr 706 . . . . . . . . . . . . . . 15 t
103102difeq1d 3293 . . . . . . . . . . . . . 14 t
104101, 103eqtr4d 2318 . . . . . . . . . . . . 13 t
105 simpr 447 . . . . . . . . . . . . . 14 t
10638ad2antrr 706 . . . . . . . . . . . . . . . . 17 t t TopOn
107 toponuni 16665 . . . . . . . . . . . . . . . . 17 t TopOn t
108106, 107syl 15 . . . . . . . . . . . . . . . 16 t t
109108difeq1d 3293 . . . . . . . . . . . . . . 15 t t
110 topontop 16664 . . . . . . . . . . . . . . . . 17 t TopOn t
111106, 110syl 15 . . . . . . . . . . . . . . . 16 t t
112 simplrr 737 . . . . . . . . . . . . . . . 16 t t
113 eqid 2283 . . . . . . . . . . . . . . . . 17 t t
114113opncld 16770 . . . . . . . . . . . . . . . 16 t t t t
115111, 112, 114syl2anc 642 . . . . . . . . . . . . . . 15 t t t
116109, 115eqeltrd 2357 . . . . . . . . . . . . . 14 t t
117 restcldr 16905 . . . . . . . . . . . . . 14 t
118105, 116, 117syl2anc 642 . . . . . . . . . . . . 13 t
119104, 118eqeltrd 2357 . . . . . . . . . . . 12 t
120 qtopcld 17404 . . . . . . . . . . . . . 14 TopOn qTop
1211, 2, 120syl2anc 642 . . . . . . . . . . . . 13 qTop
122121ad2antrr 706 . . . . . . . . . . . 12 t qTop
12397, 119, 122mpbir2and 888 . . . . . . . . . . 11 t qTop
12496a1i 10 . . . . . . . . . . 11 t
125 eqid 2283 . . . . . . . . . . . 12 qTop qTop
126125restcldi 16904 . . . . . . . . . . 11 qTop qTop qTop t
12795, 123, 124, 126syl3anc 1182 . . . . . . . . . 10 t qTop t
12890, 127eqeltrrd 2358 . . . . . . . . 9 t qTop t qTop t
129 topontop 16664 . . . . . . . . . . 11 qTop t TopOn qTop t
13087, 129syl 15 . . . . . . . . . 10 t qTop t
131 simplrl 736 . . . . . . . . . . 11 t
132131, 89sseqtrd 3214 . . . . . . . . . 10 t qTop t
133 eqid 2283 . . . . . . . . . . 11 qTop t qTop t
134133isopn2 16769 . . . . . . . . . 10 qTop t qTop t qTop t qTop t qTop t
135130, 132, 134syl2anc 642 . . . . . . . . 9 t qTop t qTop t qTop t
136128, 135mpbird 223 . . . . . . . 8 t qTop t
137 qtoprest.6 . . . . . . . . 9
138137adantr 451 . . . . . . . 8 t
13986, 136, 138mpjaodan 761 . . . . . . 7 t qTop t
140139expr 598 . . . . . 6 t qTop t
14157, 140sylbid 206 . . . . 5 t qTop t
142141expimpd 586 . . . 4 t qTop t
14348, 142sylbid 206 . . 3 t qTop qTop t
144143ssrdv 3185 . 2 t qTop qTop t
14536, 144eqssd 3196 1 qTop t t qTop
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wo 357   wa 358   wceq 1623   wcel 1684  cvv 2788   cdif 3149   cin 3151   wss 3152  cuni 3827  ccnv 4688   cdm 4689   crn 4690   cres 4691  cima 4692   wfun 5249   wfn 5250  wfo 5253  cfv 5255  (class class class)co 5858   ↾t crest 13325   qTop cqtop 13406  ctop 16631  TopOnctopon 16632  ccld 16753   ccn 16954 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-iin 3908  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-recs 6388  df-rdg 6423  df-oadd 6483  df-er 6660  df-map 6774  df-en 6864  df-fin 6867  df-fi 7165  df-rest 13327  df-topgen 13344  df-qtop 13410  df-top 16636  df-bases 16638  df-topon 16639  df-cld 16756  df-cn 16957
 Copyright terms: Public domain W3C validator