Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmscld Unicode version

Theorem cvmscld 24088
 Description: The sets of an even covering are clopen in the subspace topology on . (Contributed by Mario Carneiro, 14-Feb-2015.)
Hypothesis
Ref Expression
cvmcov.1 t t
Assertion
Ref Expression
cvmscld CovMap t
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,   ,,,   ,,
Allowed substitution hints:   (,)   (,,,)   ()

Proof of Theorem cvmscld
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cvmtop1 24075 . . . . . 6 CovMap
213ad2ant1 976 . . . . 5 CovMap
3 cvmcov.1 . . . . . . . 8 t t
43cvmsuni 24084 . . . . . . 7
543ad2ant2 977 . . . . . 6 CovMap
63cvmsss 24082 . . . . . . . 8
763ad2ant2 977 . . . . . . 7 CovMap
8 uniss 3885 . . . . . . 7
97, 8syl 15 . . . . . 6 CovMap
105, 9eqsstr3d 3247 . . . . 5 CovMap
11 eqid 2316 . . . . . 6
1211restuni 16949 . . . . 5 t
132, 10, 12syl2anc 642 . . . 4 CovMap t
1413difeq1d 3327 . . 3 CovMap t
15 unisng 3881 . . . . . . 7
16153ad2ant3 978 . . . . . 6 CovMap
1716uneq2d 3363 . . . . 5 CovMap
18 uniun 3883 . . . . . 6
19 undif1 3563 . . . . . . . . 9
20 simp3 957 . . . . . . . . . . 11 CovMap
2120snssd 3797 . . . . . . . . . 10 CovMap
22 ssequn2 3382 . . . . . . . . . 10
2321, 22sylib 188 . . . . . . . . 9 CovMap
2419, 23syl5eq 2360 . . . . . . . 8 CovMap
2524unieqd 3875 . . . . . . 7 CovMap
2625, 5eqtrd 2348 . . . . . 6 CovMap
2718, 26syl5eqr 2362 . . . . 5 CovMap
2817, 27eqtr3d 2350 . . . 4 CovMap
29 difss 3337 . . . . . . 7
30 uniss 3885 . . . . . . 7
3129, 30ax-mp 8 . . . . . 6
3231, 5syl5sseq 3260 . . . . 5 CovMap
33 uniiun 3992 . . . . . . . 8
3433ineq2i 3401 . . . . . . 7
35 incom 3395 . . . . . . 7
36 iunin2 4003 . . . . . . 7
3734, 35, 363eqtr4i 2346 . . . . . 6
38 eldifsn 3783 . . . . . . . . . 10
39 necom 2560 . . . . . . . . . . . . 13
40 df-ne 2481 . . . . . . . . . . . . 13
4139, 40bitri 240 . . . . . . . . . . . 12
423cvmsdisj 24085 . . . . . . . . . . . . . 14
43423expa 1151 . . . . . . . . . . . . 13
4443ord 366 . . . . . . . . . . . 12
4541, 44syl5bi 208 . . . . . . . . . . 11
4645impr 602 . . . . . . . . . 10
4738, 46sylan2b 461 . . . . . . . . 9
4847iuneq2dv 3963 . . . . . . . 8
49483adant1 973 . . . . . . 7 CovMap
50 iun0 3995 . . . . . . 7
5149, 50syl6eq 2364 . . . . . 6 CovMap
5237, 51syl5eq 2360 . . . . 5 CovMap
53 uneqdifeq 3576 . . . . 5
5432, 52, 53syl2anc 642 . . . 4 CovMap
5528, 54mpbid 201 . . 3 CovMap
5614, 55eqtr3d 2350 . 2 CovMap t
57 uniexg 4554 . . . . . 6
58573ad2ant2 977 . . . . 5 CovMap
595, 58eqeltrrd 2391 . . . 4 CovMap
60 resttop 16947 . . . 4 t
612, 59, 60syl2anc 642 . . 3 CovMap t
62 elssuni 3892 . . . . . . . . . . 11
6362adantl 452 . . . . . . . . . 10 CovMap
645adantr 451 . . . . . . . . . 10 CovMap
6563, 64sseqtrd 3248 . . . . . . . . 9 CovMap
66 df-ss 3200 . . . . . . . . 9
6765, 66sylib 188 . . . . . . . 8 CovMap
682adantr 451 . . . . . . . . 9 CovMap
6959adantr 451 . . . . . . . . 9 CovMap
707sselda 3214 . . . . . . . . 9 CovMap
71 elrestr 13382 . . . . . . . . 9 t
7268, 69, 70, 71syl3anc 1182 . . . . . . . 8 CovMap t
7367, 72eqeltrrd 2391 . . . . . . 7 CovMap t
7473ex 423 . . . . . 6 CovMap t
7574ssrdv 3219 . . . . 5 CovMap t
7629, 75syl5ss 3224 . . . 4 CovMap t
77 uniopn 16699 . . . 4 t t t
7861, 76, 77syl2anc 642 . . 3 CovMap t
79 eqid 2316 . . . 4 t t
8079opncld 16826 . . 3 t t t t
8161, 78, 80syl2anc 642 . 2 CovMap t t
8256, 81eqeltrrd 2391 1 CovMap t
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358   w3a 934   wceq 1633   wcel 1701   wne 2479  wral 2577  crab 2581  cvv 2822   cdif 3183   cun 3184   cin 3185   wss 3186  c0 3489  cpw 3659  csn 3674  cuni 3864  ciun 3942   cmpt 4114  ccnv 4725   cres 4728  cima 4729  cfv 5292  (class class class)co 5900   ↾t crest 13374  ctop 16687  ccld 16809   chmeo 17500   CovMap ccvm 24070 This theorem is referenced by:  cvmliftmolem1  24096  cvmlift2lem9  24126  cvmlift3lem6  24139 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-reu 2584  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-recs 6430  df-rdg 6465  df-oadd 6525  df-er 6702  df-en 6907  df-fin 6910  df-fi 7210  df-rest 13376  df-topgen 13393  df-top 16692  df-bases 16694  df-topon 16695  df-cld 16812  df-cvm 24071
 Copyright terms: Public domain W3C validator