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

Theorem qtophmeo 20909
 Description: If two functions on a base topology make the same identifications in order to create quotient spaces qTop and qTop , then not only are qTop and qTop homeomorphic, but there is a unique homeomorphism that makes the diagram commute. (Contributed by Mario Carneiro, 24-Mar-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
Hypotheses
Ref Expression
qtophmeo.2 TopOn
qtophmeo.3
qtophmeo.4
qtophmeo.5
Assertion
Ref Expression
qtophmeo qTop qTop
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,   ,,   ,,
Allowed substitution hints:   ()   ()

Proof of Theorem qtophmeo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qtophmeo.2 . . . . 5 TopOn
2 qtophmeo.3 . . . . 5
3 qtophmeo.4 . . . . . . 7
4 fofn 5808 . . . . . . 7
53, 4syl 17 . . . . . 6
6 qtopid 20797 . . . . . 6 TopOn qTop
71, 5, 6syl2anc 673 . . . . 5 qTop
8 df-3an 1009 . . . . . 6
9 qtophmeo.5 . . . . . . . 8
109biimpd 212 . . . . . . 7
1110impr 631 . . . . . 6
128, 11sylan2b 483 . . . . 5
131, 2, 7, 12qtopeu 20808 . . . 4 qTop qTop
14 reurex 2995 . . . 4 qTop qTop qTop qTop
1513, 14syl 17 . . 3 qTop qTop
16 simprl 772 . . . . . . 7 qTop qTop qTop qTop
17 fofn 5808 . . . . . . . . . . . . 13
182, 17syl 17 . . . . . . . . . . . 12
19 qtopid 20797 . . . . . . . . . . . 12 TopOn qTop
201, 18, 19syl2anc 673 . . . . . . . . . . 11 qTop
21 df-3an 1009 . . . . . . . . . . . 12
229biimprd 231 . . . . . . . . . . . . 13
2322impr 631 . . . . . . . . . . . 12
2421, 23sylan2b 483 . . . . . . . . . . 11
251, 3, 20, 24qtopeu 20808 . . . . . . . . . 10 qTop qTop
2625adantr 472 . . . . . . . . 9 qTop qTop qTop qTop
27 reurex 2995 . . . . . . . . 9 qTop qTop qTop qTop
2826, 27syl 17 . . . . . . . 8 qTop qTop qTop qTop
29 qtoptopon 20796 . . . . . . . . . . . . 13 TopOn qTop TopOn
301, 2, 29syl2anc 673 . . . . . . . . . . . 12 qTop TopOn
3130ad2antrr 740 . . . . . . . . . . 11 qTop qTop qTop qTop qTop TopOn
32 qtoptopon 20796 . . . . . . . . . . . . 13 TopOn qTop TopOn
331, 3, 32syl2anc 673 . . . . . . . . . . . 12 qTop TopOn
3433ad2antrr 740 . . . . . . . . . . 11 qTop qTop qTop qTop qTop TopOn
35 simplrl 778 . . . . . . . . . . 11 qTop qTop qTop qTop qTop qTop
36 cnf2 20342 . . . . . . . . . . 11 qTop TopOn qTop TopOn qTop qTop
3731, 34, 35, 36syl3anc 1292 . . . . . . . . . 10 qTop qTop qTop qTop
38 simprl 772 . . . . . . . . . . 11 qTop qTop qTop qTop qTop qTop
39 cnf2 20342 . . . . . . . . . . 11 qTop TopOn qTop TopOn qTop qTop
4034, 31, 38, 39syl3anc 1292 . . . . . . . . . 10 qTop qTop qTop qTop
41 coeq1 4997 . . . . . . . . . . . 12
4241eqeq2d 2481 . . . . . . . . . . 11
43 coeq1 4997 . . . . . . . . . . . 12
4443eqeq2d 2481 . . . . . . . . . . 11
45 simpr3 1038 . . . . . . . . . . . . 13
461, 2, 20, 45qtopeu 20808 . . . . . . . . . . . 12 qTop qTop
4746ad2antrr 740 . . . . . . . . . . 11 qTop qTop qTop qTop qTop qTop
48 cnco 20359 . . . . . . . . . . . 12 qTop qTop qTop qTop qTop qTop
4935, 38, 48syl2anc 673 . . . . . . . . . . 11 qTop qTop qTop qTop qTop qTop
50 idcn 20350 . . . . . . . . . . . . 13 qTop TopOn qTop qTop
5130, 50syl 17 . . . . . . . . . . . 12 qTop qTop
5251ad2antrr 740 . . . . . . . . . . 11 qTop qTop qTop qTop qTop qTop
53 simprr 774 . . . . . . . . . . . . 13 qTop qTop qTop qTop
54 simplrr 779 . . . . . . . . . . . . . 14 qTop qTop qTop qTop
5554coeq2d 5002 . . . . . . . . . . . . 13 qTop qTop qTop qTop
5653, 55eqtrd 2505 . . . . . . . . . . . 12 qTop qTop qTop qTop
57 coass 5361 . . . . . . . . . . . 12
5856, 57syl6eqr 2523 . . . . . . . . . . 11 qTop qTop qTop qTop
59 fof 5806 . . . . . . . . . . . . . . 15
602, 59syl 17 . . . . . . . . . . . . . 14
6160ad2antrr 740 . . . . . . . . . . . . 13 qTop qTop qTop qTop
62 fcoi2 5770 . . . . . . . . . . . . 13
6361, 62syl 17 . . . . . . . . . . . 12 qTop qTop qTop qTop
6463eqcomd 2477 . . . . . . . . . . 11 qTop qTop qTop qTop
6542, 44, 47, 49, 52, 58, 64reu2eqd 3223 . . . . . . . . . 10 qTop qTop qTop qTop
66 coeq1 4997 . . . . . . . . . . . 12
6766eqeq2d 2481 . . . . . . . . . . 11
68 coeq1 4997 . . . . . . . . . . . 12
6968eqeq2d 2481 . . . . . . . . . . 11
70 simpr3 1038 . . . . . . . . . . . . 13
711, 3, 7, 70qtopeu 20808 . . . . . . . . . . . 12 qTop qTop
7271ad2antrr 740 . . . . . . . . . . 11 qTop qTop qTop qTop qTop qTop
73 cnco 20359 . . . . . . . . . . . 12 qTop qTop qTop qTop qTop qTop
7438, 35, 73syl2anc 673 . . . . . . . . . . 11 qTop qTop qTop qTop qTop qTop
75 idcn 20350 . . . . . . . . . . . . 13 qTop TopOn qTop qTop
7633, 75syl 17 . . . . . . . . . . . 12 qTop qTop
7776ad2antrr 740 . . . . . . . . . . 11 qTop qTop qTop qTop qTop qTop
7853coeq2d 5002 . . . . . . . . . . . . 13 qTop qTop qTop qTop
7954, 78eqtrd 2505 . . . . . . . . . . . 12 qTop qTop qTop qTop
80 coass 5361 . . . . . . . . . . . 12
8179, 80syl6eqr 2523 . . . . . . . . . . 11 qTop qTop qTop qTop
82 fof 5806 . . . . . . . . . . . . . . 15
833, 82syl 17 . . . . . . . . . . . . . 14
8483ad2antrr 740 . . . . . . . . . . . . 13 qTop qTop qTop qTop
85 fcoi2 5770 . . . . . . . . . . . . 13
8684, 85syl 17 . . . . . . . . . . . 12 qTop qTop qTop qTop
8786eqcomd 2477 . . . . . . . . . . 11 qTop qTop qTop qTop
8867, 69, 72, 74, 77, 81, 87reu2eqd 3223 . . . . . . . . . 10 qTop qTop qTop qTop
8937, 40, 65, 882fcoidinvd 6211 . . . . . . . . 9 qTop qTop qTop qTop
9089, 38eqeltrd 2549 . . . . . . . 8 qTop qTop qTop qTop qTop qTop
9128, 90rexlimddv 2875 . . . . . . 7 qTop qTop qTop qTop
92 ishmeo 20851 . . . . . . 7 qTop qTop qTop qTop qTop qTop
9316, 91, 92sylanbrc 677 . . . . . 6 qTop qTop qTop qTop
94 simprr 774 . . . . . 6 qTop qTop
9593, 94jca 541 . . . . 5 qTop qTop qTop qTop
9695ex 441 . . . 4 qTop qTop qTop qTop
9796reximdv2 2855 . . 3 qTop qTop qTop qTop
9815, 97mpd 15 . 2 qTop qTop
99 eqtr2 2491 . . . 4
1002adantr 472 . . . . 5 qTop qTop qTop qTop
10130adantr 472 . . . . . . 7 qTop qTop qTop qTop qTop TopOn
10233adantr 472 . . . . . . 7 qTop qTop qTop qTop qTop TopOn
103 simprl 772 . . . . . . 7 qTop qTop qTop qTop qTop qTop
104 hmeof1o2 20855 . . . . . . 7 qTop TopOn qTop TopOn qTop qTop
105101, 102, 103, 104syl3anc 1292 . . . . . 6 qTop qTop qTop qTop
106 f1ofn 5829 . . . . . 6
107105, 106syl 17 . . . . 5 qTop qTop qTop qTop
108 simprr 774 . . . . . . 7 qTop qTop qTop qTop qTop qTop
109 hmeof1o2 20855 . . . . . . 7 qTop TopOn qTop TopOn qTop qTop
110101, 102, 108, 109syl3anc 1292 . . . . . 6 qTop qTop qTop qTop
111 f1ofn 5829 . . . . . 6
112110, 111syl 17 . . . . 5 qTop qTop qTop qTop
113 cocan2 6208 . . . . 5
114100, 107, 112, 113syl3anc 1292 . . . 4 qTop qTop qTop qTop
11599, 114syl5ib 227 . . 3 qTop qTop qTop qTop
116115ralrimivva 2814 . 2 qTop qTop qTop qTop
117 coeq1 4997 . . . 4
118117eqeq2d 2481 . . 3
119118reu4 3220 . 2 qTop qTop qTop qTop qTop qTop qTop qTop
12098, 116, 119sylanbrc 677 1 qTop qTop
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   w3a 1007   wceq 1452   wcel 1904  wral 2756  wrex 2757  wreu 2758   cid 4749  ccnv 4838   cres 4841   ccom 4843   wfn 5584  wf 5585  wfo 5587  wf1o 5588  cfv 5589  (class class class)co 6308   qTop cqtop 15479  TopOnctopon 19995   ccn 20317  chmeo 20845 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-map 7492  df-qtop 15484  df-top 19998  df-topon 20000  df-cn 20320  df-hmeo 20847 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator