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

Theorem isr0 17771
 Description: The property " is an R0 space". A space is R0 if any two topologically distinguishable points are separated (there is an open set containing each one and disjoint from the other). Or in contraposition, if every open set which contains also contains , so there is no separation, then and are members of the same open sets. We have chosen not to give this definition a name, because it turns out that a space is R0 if and only if its Kolmogorov quotient is T1, so that is what we prove here. (Contributed by Mario Carneiro, 25-Aug-2015.)
Hypothesis
Ref Expression
kqval.2
Assertion
Ref Expression
isr0 TopOn KQ
Distinct variable groups:   ,,,,,   ,,,   ,,,,,
Allowed substitution hints:   (,)

Proof of Theorem isr0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 kqval.2 . . . . . . . . . . . 12
21kqid 17762 . . . . . . . . . . 11 TopOn KQ
32ad2antrr 708 . . . . . . . . . 10 TopOn KQ KQ
4 cnima 17331 . . . . . . . . . 10 KQ KQ
53, 4sylan 459 . . . . . . . . 9 TopOn KQ KQ
6 eleq2 2499 . . . . . . . . . . 11
7 eleq2 2499 . . . . . . . . . . 11
86, 7imbi12d 313 . . . . . . . . . 10
98rspcv 3050 . . . . . . . . 9
105, 9syl 16 . . . . . . . 8 TopOn KQ KQ
111kqffn 17759 . . . . . . . . . . . . 13 TopOn
1211ad2antrr 708 . . . . . . . . . . . 12 TopOn KQ
1312adantr 453 . . . . . . . . . . 11 TopOn KQ KQ
14 fnfun 5544 . . . . . . . . . . 11
1513, 14syl 16 . . . . . . . . . 10 TopOn KQ KQ
16 simprl 734 . . . . . . . . . . . 12 TopOn KQ
1716adantr 453 . . . . . . . . . . 11 TopOn KQ KQ
18 fndm 5546 . . . . . . . . . . . 12
1913, 18syl 16 . . . . . . . . . . 11 TopOn KQ KQ
2017, 19eleqtrrd 2515 . . . . . . . . . 10 TopOn KQ KQ
21 fvimacnv 5847 . . . . . . . . . 10
2215, 20, 21syl2anc 644 . . . . . . . . 9 TopOn KQ KQ
23 simprr 735 . . . . . . . . . . . 12 TopOn KQ
2423adantr 453 . . . . . . . . . . 11 TopOn KQ KQ
2524, 19eleqtrrd 2515 . . . . . . . . . 10 TopOn KQ KQ
26 fvimacnv 5847 . . . . . . . . . 10
2715, 25, 26syl2anc 644 . . . . . . . . 9 TopOn KQ KQ
2822, 27imbi12d 313 . . . . . . . 8 TopOn KQ KQ
2910, 28sylibrd 227 . . . . . . 7 TopOn KQ KQ
3029ralrimdva 2798 . . . . . 6 TopOn KQ KQ
31 simplr 733 . . . . . . 7 TopOn KQ KQ
32 fnfvelrn 5869 . . . . . . . . 9
3312, 16, 32syl2anc 644 . . . . . . . 8 TopOn KQ
341kqtopon 17761 . . . . . . . . . 10 TopOn KQ TopOn
3534ad2antrr 708 . . . . . . . . 9 TopOn KQ KQ TopOn
36 toponuni 16994 . . . . . . . . 9 KQ TopOn KQ
3735, 36syl 16 . . . . . . . 8 TopOn KQ KQ
3833, 37eleqtrd 2514 . . . . . . 7 TopOn KQ KQ
39 fnfvelrn 5869 . . . . . . . . 9
4012, 23, 39syl2anc 644 . . . . . . . 8 TopOn KQ
4140, 37eleqtrd 2514 . . . . . . 7 TopOn KQ KQ
42 eqid 2438 . . . . . . . 8 KQ KQ
4342t1sep2 17435 . . . . . . 7 KQ KQ KQ KQ
4431, 38, 41, 43syl3anc 1185 . . . . . 6 TopOn KQ KQ
4530, 44syld 43 . . . . 5 TopOn KQ
461kqfeq 17758 . . . . . . . 8 TopOn
47 eleq2 2499 . . . . . . . . . 10
48 eleq2 2499 . . . . . . . . . 10
4947, 48bibi12d 314 . . . . . . . . 9
5049cbvralv 2934 . . . . . . . 8
5146, 50syl6bbr 256 . . . . . . 7 TopOn
52513expb 1155 . . . . . 6 TopOn
5352adantlr 697 . . . . 5 TopOn KQ
5445, 53sylibd 207 . . . 4 TopOn KQ
5554ralrimivva 2800 . . 3 TopOn KQ
5655ex 425 . 2 TopOn KQ
57 simpll 732 . . . . . . . . . . 11 TopOn TopOn
581kqopn 17768 . . . . . . . . . . 11 TopOn KQ
5957, 58sylan 459 . . . . . . . . . 10 TopOn KQ
60 eleq2 2499 . . . . . . . . . . . 12
61 eleq2 2499 . . . . . . . . . . . 12
6260, 61imbi12d 313 . . . . . . . . . . 11
6362rspcv 3050 . . . . . . . . . 10 KQ KQ
6459, 63syl 16 . . . . . . . . 9 TopOn KQ
651kqfvima 17764 . . . . . . . . . . . . 13 TopOn
66653expa 1154 . . . . . . . . . . . 12 TopOn
6766an32s 781 . . . . . . . . . . 11 TopOn
6867adantlr 697 . . . . . . . . . 10 TopOn
691kqfvima 17764 . . . . . . . . . . . . 13 TopOn
70693expa 1154 . . . . . . . . . . . 12 TopOn
7170an32s 781 . . . . . . . . . . 11 TopOn
7271adantllr 701 . . . . . . . . . 10 TopOn
7368, 72imbi12d 313 . . . . . . . . 9 TopOn
7464, 73sylibrd 227 . . . . . . . 8 TopOn KQ
7574ralrimdva 2798 . . . . . . 7 TopOn KQ
761kqfval 17757 . . . . . . . . . . 11 TopOn
7776adantr 453 . . . . . . . . . 10 TopOn
781kqfval 17757 . . . . . . . . . . 11 TopOn
7978adantlr 697 . . . . . . . . . 10 TopOn
8077, 79eqeq12d 2452 . . . . . . . . 9 TopOn
81 rabbi 2888 . . . . . . . . . 10
8250, 81bitri 242 . . . . . . . . 9
8380, 82syl6bbr 256 . . . . . . . 8 TopOn
8483biimprd 216 . . . . . . 7 TopOn
8575, 84imim12d 71 . . . . . 6 TopOn KQ
8685ralimdva 2786 . . . . 5 TopOn KQ
8786ralimdva 2786 . . . 4 TopOn KQ
88 eleq1 2498 . . . . . . . . . . 11
8988imbi1d 310 . . . . . . . . . 10
9089ralbidv 2727 . . . . . . . . 9 KQ KQ
91 eqeq1 2444 . . . . . . . . 9
9290, 91imbi12d 313 . . . . . . . 8 KQ KQ
9392ralbidv 2727 . . . . . . 7 KQ KQ
9493ralrn 5875 . . . . . 6 KQ KQ
95 eleq1 2498 . . . . . . . . . . 11
9695imbi2d 309 . . . . . . . . . 10
9796ralbidv 2727 . . . . . . . . 9 KQ KQ
98 eqeq2 2447 . . . . . . . . 9
9997, 98imbi12d 313 . . . . . . . 8 KQ KQ
10099ralrn 5875 . . . . . . 7 KQ KQ
101100ralbidv 2727 . . . . . 6 KQ KQ
10294, 101bitrd 246 . . . . 5 KQ KQ
10311, 102syl 16 . . . 4 TopOn KQ KQ
10487, 103sylibrd 227 . . 3 TopOn KQ
105 ist1-2 17413 . . . 4 KQ TopOn KQ KQ
10634, 105syl 16 . . 3 TopOn KQ KQ
107104, 106sylibrd 227 . 2 TopOn KQ
10856, 107impbid 185 1 TopOn KQ
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   w3a 937   wceq 1653   wcel 1726  wral 2707  crab 2711  cuni 4017   cmpt 4268  ccnv 4879   cdm 4880   crn 4881  cima 4883   wfun 5450   wfn 5451  cfv 5456  (class class class)co 6083  TopOnctopon 16961   ccn 17290  ct1 17373  KQckq 17727 This theorem is referenced by:  r0sep  17782 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-map 7022  df-topgen 13669  df-qtop 13735  df-top 16965  df-topon 16968  df-cld 17085  df-cn 17293  df-t1 17380  df-kq 17728
 Copyright terms: Public domain W3C validator