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

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

Proof of Theorem kqreglem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 topontop 19928 . . 3 TopOn
21adantr 466 . 2 TopOn KQ
3 simplr 760 . . . . 5 TopOn KQ KQ
4 simpll 758 . . . . . 6 TopOn KQ TopOn
5 simprl 762 . . . . . 6 TopOn KQ
6 kqval.2 . . . . . . 7
76kqopn 20736 . . . . . 6 TopOn KQ
84, 5, 7syl2anc 665 . . . . 5 TopOn KQ KQ
9 simprr 764 . . . . . 6 TopOn KQ
10 toponss 19931 . . . . . . . . 9 TopOn
114, 5, 10syl2anc 665 . . . . . . . 8 TopOn KQ
1211, 9sseldd 3465 . . . . . . 7 TopOn KQ
136kqfvima 20732 . . . . . . 7 TopOn
144, 5, 12, 13syl3anc 1264 . . . . . 6 TopOn KQ
159, 14mpbid 213 . . . . 5 TopOn KQ
16 regsep 20337 . . . . 5 KQ KQ KQ KQ
173, 8, 15, 16syl3anc 1264 . . . 4 TopOn KQ KQ KQ
184adantr 466 . . . . . . 7 TopOn KQ KQ KQ TopOn
196kqid 20730 . . . . . . 7 TopOn KQ
2018, 19syl 17 . . . . . 6 TopOn KQ KQ KQ KQ
21 simprl 762 . . . . . 6 TopOn KQ KQ KQ KQ
22 cnima 20268 . . . . . 6 KQ KQ
2320, 21, 22syl2anc 665 . . . . 5 TopOn KQ KQ KQ
2412adantr 466 . . . . . 6 TopOn KQ KQ KQ
25 simprrl 772 . . . . . 6 TopOn KQ KQ KQ
266kqffn 20727 . . . . . . 7 TopOn
27 elpreima 6014 . . . . . . 7
2818, 26, 273syl 18 . . . . . 6 TopOn KQ KQ KQ
2924, 25, 28mpbir2and 930 . . . . 5 TopOn KQ KQ KQ
306kqtopon 20729 . . . . . . . . . 10 TopOn KQ TopOn
31 topontop 19928 . . . . . . . . . 10 KQ TopOn KQ
3218, 30, 313syl 18 . . . . . . . . 9 TopOn KQ KQ KQ KQ
33 elssuni 4245 . . . . . . . . . 10 KQ KQ
3433ad2antrl 732 . . . . . . . . 9 TopOn KQ KQ KQ KQ
35 eqid 2422 . . . . . . . . . 10 KQ KQ
3635clscld 20049 . . . . . . . . 9 KQ KQ KQ KQ
3732, 34, 36syl2anc 665 . . . . . . . 8 TopOn KQ KQ KQ KQ KQ
38 cnclima 20271 . . . . . . . 8 KQ KQ KQ KQ
3920, 37, 38syl2anc 665 . . . . . . 7 TopOn KQ KQ KQ KQ
4035sscls 20058 . . . . . . . . 9 KQ KQ KQ
4132, 34, 40syl2anc 665 . . . . . . . 8 TopOn KQ KQ KQ KQ
42 imass2 5220 . . . . . . . 8 KQ KQ
4341, 42syl 17 . . . . . . 7 TopOn KQ KQ KQ KQ
44 eqid 2422 . . . . . . . 8
4544clsss2 20075 . . . . . . 7 KQ KQ KQ
4639, 43, 45syl2anc 665 . . . . . 6 TopOn KQ KQ KQ KQ
47 simprrr 773 . . . . . . . 8 TopOn KQ KQ KQ KQ
48 imass2 5220 . . . . . . . 8 KQ KQ
4947, 48syl 17 . . . . . . 7 TopOn KQ KQ KQ KQ
505adantr 466 . . . . . . . 8 TopOn KQ KQ KQ
516kqsat 20733 . . . . . . . 8 TopOn
5218, 50, 51syl2anc 665 . . . . . . 7 TopOn KQ KQ KQ
5349, 52sseqtrd 3500 . . . . . 6 TopOn KQ KQ KQ KQ
5446, 53sstrd 3474 . . . . 5 TopOn KQ KQ KQ
55 eleq2 2495 . . . . . . 7
56 fveq2 5878 . . . . . . . 8
5756sseq1d 3491 . . . . . . 7
5855, 57anbi12d 715 . . . . . 6
5958rspcev 3182 . . . . 5
6023, 29, 54, 59syl12anc 1262 . . . 4 TopOn KQ KQ KQ
6117, 60rexlimddv 2921 . . 3 TopOn KQ
6261ralrimivva 2846 . 2 TopOn KQ
63 isreg 20335 . 2
642, 62, 63sylanbrc 668 1 TopOn KQ
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   wceq 1437   wcel 1868  wral 2775  wrex 2776  crab 2779   wss 3436  cuni 4216   cmpt 4479  ccnv 4849   crn 4851  cima 4853   wfn 5593  cfv 5598  (class class class)co 6302  ctop 19904  TopOnctopon 19905  ccld 20018  ccl 20020   ccn 20227  creg 20312  KQckq 20695 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 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-iin 4299  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-map 7479  df-qtop 15394  df-top 19908  df-topon 19910  df-cld 20021  df-cls 20023  df-cn 20230  df-reg 20319  df-kq 20696 This theorem is referenced by:  kqreg  20753
 Copyright terms: Public domain W3C validator