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

Theorem kqnrmlem2 17541
 Description: If the Kolmogorov quotient of a space is normal then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.)
Hypothesis
Ref Expression
kqval.2
Assertion
Ref Expression
kqnrmlem2 TopOn KQ
Distinct variable groups:   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem kqnrmlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 topontop 16770 . . 3 TopOn
21adantr 451 . 2 TopOn KQ
3 simplr 731 . . . . 5 TopOn KQ KQ
4 simpll 730 . . . . . 6 TopOn KQ TopOn
5 simprl 732 . . . . . 6 TopOn KQ
6 kqval.2 . . . . . . 7
76kqopn 17531 . . . . . 6 TopOn KQ
84, 5, 7syl2anc 642 . . . . 5 TopOn KQ KQ
9 inss1 3465 . . . . . . 7
10 simprr 733 . . . . . . 7 TopOn KQ
119, 10sseldi 3254 . . . . . 6 TopOn KQ
126kqcld 17532 . . . . . 6 TopOn KQ
134, 11, 12syl2anc 642 . . . . 5 TopOn KQ KQ
14 inss2 3466 . . . . . . 7
1514, 10sseldi 3254 . . . . . 6 TopOn KQ
16 elpwi 3709 . . . . . 6
17 imass2 5131 . . . . . 6
1815, 16, 173syl 18 . . . . 5 TopOn KQ
19 nrmsep3 17189 . . . . 5 KQ KQ KQ KQ KQ
203, 8, 13, 18, 19syl13anc 1184 . . . 4 TopOn KQ KQ KQ
21 simplll 734 . . . . . . . . 9 TopOn KQ KQ KQ TopOn
226kqid 17525 . . . . . . . . 9 TopOn KQ
2321, 22syl 15 . . . . . . . 8 TopOn KQ KQ KQ KQ
24 simprl 732 . . . . . . . 8 TopOn KQ KQ KQ KQ
25 cnima 17100 . . . . . . . 8 KQ KQ
2623, 24, 25syl2anc 642 . . . . . . 7 TopOn KQ KQ KQ
27 simprrl 740 . . . . . . . 8 TopOn KQ KQ KQ
286kqffn 17522 . . . . . . . . . 10 TopOn
29 fnfun 5423 . . . . . . . . . 10
3021, 28, 293syl 18 . . . . . . . . 9 TopOn KQ KQ KQ
3111adantr 451 . . . . . . . . . . 11 TopOn KQ KQ KQ
32 eqid 2358 . . . . . . . . . . . 12
3332cldss 16872 . . . . . . . . . . 11
3431, 33syl 15 . . . . . . . . . 10 TopOn KQ KQ KQ
35 fndm 5425 . . . . . . . . . . . 12
3621, 28, 353syl 18 . . . . . . . . . . 11 TopOn KQ KQ KQ
37 toponuni 16771 . . . . . . . . . . . 12 TopOn
3821, 37syl 15 . . . . . . . . . . 11 TopOn KQ KQ KQ
3936, 38eqtrd 2390 . . . . . . . . . 10 TopOn KQ KQ KQ
4034, 39sseqtr4d 3291 . . . . . . . . 9 TopOn KQ KQ KQ
41 funimass3 5724 . . . . . . . . 9
4230, 40, 41syl2anc 642 . . . . . . . 8 TopOn KQ KQ KQ
4327, 42mpbid 201 . . . . . . 7 TopOn KQ KQ KQ
446kqtopon 17524 . . . . . . . . . . . 12 TopOn KQ TopOn
45 topontop 16770 . . . . . . . . . . . 12 KQ TopOn KQ
4621, 44, 453syl 18 . . . . . . . . . . 11 TopOn KQ KQ KQ KQ
47 elssuni 3936 . . . . . . . . . . . 12 KQ KQ
4847ad2antrl 708 . . . . . . . . . . 11 TopOn KQ KQ KQ KQ
49 eqid 2358 . . . . . . . . . . . 12 KQ KQ
5049clscld 16890 . . . . . . . . . . 11 KQ KQ KQ KQ
5146, 48, 50syl2anc 642 . . . . . . . . . 10 TopOn KQ KQ KQ KQ KQ
52 cnclima 17103 . . . . . . . . . 10 KQ KQ KQ KQ
5323, 51, 52syl2anc 642 . . . . . . . . 9 TopOn KQ KQ KQ KQ
5449sscls 16899 . . . . . . . . . . 11 KQ KQ KQ
5546, 48, 54syl2anc 642 . . . . . . . . . 10 TopOn KQ KQ KQ KQ
56 imass2 5131 . . . . . . . . . 10 KQ KQ
5755, 56syl 15 . . . . . . . . 9 TopOn KQ KQ KQ KQ
5832clsss2 16915 . . . . . . . . 9 KQ KQ KQ
5953, 57, 58syl2anc 642 . . . . . . . 8 TopOn KQ KQ KQ KQ
60 simprrr 741 . . . . . . . . . 10 TopOn KQ KQ KQ KQ
61 imass2 5131 . . . . . . . . . 10 KQ KQ
6260, 61syl 15 . . . . . . . . 9 TopOn KQ KQ KQ KQ
635adantr 451 . . . . . . . . . 10 TopOn KQ KQ KQ
646kqsat 17528 . . . . . . . . . 10 TopOn
6521, 63, 64syl2anc 642 . . . . . . . . 9 TopOn KQ KQ KQ
6662, 65sseqtrd 3290 . . . . . . . 8 TopOn KQ KQ KQ KQ
6759, 66sstrd 3265 . . . . . . 7 TopOn KQ KQ KQ
68 sseq2 3276 . . . . . . . . 9
69 fveq2 5608 . . . . . . . . . 10
7069sseq1d 3281 . . . . . . . . 9
7168, 70anbi12d 691 . . . . . . . 8
7271rspcev 2960 . . . . . . 7
7326, 43, 67, 72syl12anc 1180 . . . . . 6 TopOn KQ KQ KQ
7473expr 598 . . . . 5 TopOn KQ KQ KQ
7574rexlimdva 2743 . . . 4 TopOn KQ KQ KQ
7620, 75mpd 14 . . 3 TopOn KQ
7776ralrimivva 2711 . 2 TopOn KQ
78 isnrm 17169 . 2
792, 77, 78sylanbrc 645 1 TopOn KQ
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   wceq 1642   wcel 1710  wral 2619  wrex 2620  crab 2623   cin 3227   wss 3228  cpw 3701  cuni 3908   cmpt 4158  ccnv 4770   cdm 4771   crn 4772  cima 4774   wfun 5331   wfn 5332  cfv 5337  (class class class)co 5945  ctop 16737  TopOnctopon 16738  ccld 16859  ccl 16861   ccn 17060  cnrm 17144  KQckq 17490 This theorem is referenced by:  kqnrm  17549 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4212  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-int 3944  df-iun 3988  df-iin 3989  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-map 6862  df-qtop 13509  df-top 16742  df-topon 16745  df-cld 16862  df-cls 16864  df-cn 17063  df-nrm 17151  df-kq 17491
 Copyright terms: Public domain W3C validator