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

Theorem kqnrmlem2 20771
 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 19953 . . 3 TopOn
21adantr 467 . 2 TopOn KQ
3 simplr 763 . . . . 5 TopOn KQ KQ
4 simpll 761 . . . . . 6 TopOn KQ TopOn
5 simprl 765 . . . . . 6 TopOn KQ
6 kqval.2 . . . . . . 7
76kqopn 20761 . . . . . 6 TopOn KQ
84, 5, 7syl2anc 667 . . . . 5 TopOn KQ KQ
9 inss1 3654 . . . . . . 7
10 simprr 767 . . . . . . 7 TopOn KQ
119, 10sseldi 3432 . . . . . 6 TopOn KQ
126kqcld 20762 . . . . . 6 TopOn KQ
134, 11, 12syl2anc 667 . . . . 5 TopOn KQ KQ
14 inss2 3655 . . . . . . 7
1514, 10sseldi 3432 . . . . . 6 TopOn KQ
16 elpwi 3962 . . . . . 6
17 imass2 5207 . . . . . 6
1815, 16, 173syl 18 . . . . 5 TopOn KQ
19 nrmsep3 20383 . . . . 5 KQ KQ KQ KQ KQ
203, 8, 13, 18, 19syl13anc 1271 . . . 4 TopOn KQ KQ KQ
21 simplll 769 . . . . . . 7 TopOn KQ KQ KQ TopOn
226kqid 20755 . . . . . . 7 TopOn KQ
2321, 22syl 17 . . . . . 6 TopOn KQ KQ KQ KQ
24 simprl 765 . . . . . 6 TopOn KQ KQ KQ KQ
25 cnima 20293 . . . . . 6 KQ KQ
2623, 24, 25syl2anc 667 . . . . 5 TopOn KQ KQ KQ
27 simprrl 775 . . . . . 6 TopOn KQ KQ KQ
286kqffn 20752 . . . . . . . 8 TopOn
29 fnfun 5678 . . . . . . . 8
3021, 28, 293syl 18 . . . . . . 7 TopOn KQ KQ KQ
3111adantr 467 . . . . . . . . 9 TopOn KQ KQ KQ
32 eqid 2453 . . . . . . . . . 10
3332cldss 20056 . . . . . . . . 9
3431, 33syl 17 . . . . . . . 8 TopOn KQ KQ KQ
35 fndm 5680 . . . . . . . . . 10
3621, 28, 353syl 18 . . . . . . . . 9 TopOn KQ KQ KQ
37 toponuni 19954 . . . . . . . . . 10 TopOn
3821, 37syl 17 . . . . . . . . 9 TopOn KQ KQ KQ
3936, 38eqtrd 2487 . . . . . . . 8 TopOn KQ KQ KQ
4034, 39sseqtr4d 3471 . . . . . . 7 TopOn KQ KQ KQ
41 funimass3 6003 . . . . . . 7
4230, 40, 41syl2anc 667 . . . . . 6 TopOn KQ KQ KQ
4327, 42mpbid 214 . . . . 5 TopOn KQ KQ KQ
446kqtopon 20754 . . . . . . . . . 10 TopOn KQ TopOn
45 topontop 19953 . . . . . . . . . 10 KQ TopOn KQ
4621, 44, 453syl 18 . . . . . . . . 9 TopOn KQ KQ KQ KQ
47 elssuni 4230 . . . . . . . . . 10 KQ KQ
4847ad2antrl 735 . . . . . . . . 9 TopOn KQ KQ KQ KQ
49 eqid 2453 . . . . . . . . . 10 KQ KQ
5049clscld 20074 . . . . . . . . 9 KQ KQ KQ KQ
5146, 48, 50syl2anc 667 . . . . . . . 8 TopOn KQ KQ KQ KQ KQ
52 cnclima 20296 . . . . . . . 8 KQ KQ KQ KQ
5323, 51, 52syl2anc 667 . . . . . . 7 TopOn KQ KQ KQ KQ
5449sscls 20083 . . . . . . . . 9 KQ KQ KQ
5546, 48, 54syl2anc 667 . . . . . . . 8 TopOn KQ KQ KQ KQ
56 imass2 5207 . . . . . . . 8 KQ KQ
5755, 56syl 17 . . . . . . 7 TopOn KQ KQ KQ KQ
5832clsss2 20100 . . . . . . 7 KQ KQ KQ
5953, 57, 58syl2anc 667 . . . . . 6 TopOn KQ KQ KQ KQ
60 simprrr 776 . . . . . . . 8 TopOn KQ KQ KQ KQ
61 imass2 5207 . . . . . . . 8 KQ KQ
6260, 61syl 17 . . . . . . 7 TopOn KQ KQ KQ KQ
635adantr 467 . . . . . . . 8 TopOn KQ KQ KQ
646kqsat 20758 . . . . . . . 8 TopOn
6521, 63, 64syl2anc 667 . . . . . . 7 TopOn KQ KQ KQ
6662, 65sseqtrd 3470 . . . . . 6 TopOn KQ KQ KQ KQ
6759, 66sstrd 3444 . . . . 5 TopOn KQ KQ KQ
68 sseq2 3456 . . . . . . 7
69 fveq2 5870 . . . . . . . 8
7069sseq1d 3461 . . . . . . 7
7168, 70anbi12d 718 . . . . . 6
7271rspcev 3152 . . . . 5
7326, 43, 67, 72syl12anc 1267 . . . 4 TopOn KQ KQ KQ
7420, 73rexlimddv 2885 . . 3 TopOn KQ
7574ralrimivva 2811 . 2 TopOn KQ
76 isnrm 20363 . 2
772, 75, 76sylanbrc 671 1 TopOn KQ
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1446   wcel 1889  wral 2739  wrex 2740  crab 2743   cin 3405   wss 3406  cpw 3953  cuni 4201   cmpt 4464  ccnv 4836   cdm 4837   crn 4838  cima 4840   wfun 5579   wfn 5580  cfv 5585  (class class class)co 6295  ctop 19929  TopOnctopon 19930  ccld 20043  ccl 20045   ccn 20252  cnrm 20338  KQckq 20720 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-iin 4284  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-map 7479  df-qtop 15418  df-top 19933  df-topon 19935  df-cld 20046  df-cls 20048  df-cn 20255  df-nrm 20345  df-kq 20721 This theorem is referenced by:  kqnrm  20779
 Copyright terms: Public domain W3C validator