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

Theorem cvmsss2 24953
 Description: An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.)
Hypothesis
Ref Expression
cvmcov.1 t t
Assertion
Ref Expression
cvmsss2 CovMap
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,
Allowed substitution hints:   (,,,)

Proof of Theorem cvmsss2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0 3629 . 2
2 simpl2 961 . . . . . 6 CovMap
3 simpl1 960 . . . . . . . . . . . 12 CovMap CovMap
4 cvmtop1 24939 . . . . . . . . . . . 12 CovMap
53, 4syl 16 . . . . . . . . . . 11 CovMap
65adantr 452 . . . . . . . . . 10 CovMap
7 cvmcov.1 . . . . . . . . . . . . 13 t t
87cvmsss 24946 . . . . . . . . . . . 12
98adantl 453 . . . . . . . . . . 11 CovMap
109sselda 3340 . . . . . . . . . 10 CovMap
11 cvmcn 24941 . . . . . . . . . . . . 13 CovMap
123, 11syl 16 . . . . . . . . . . . 12 CovMap
13 cnima 17321 . . . . . . . . . . . 12
1412, 2, 13syl2anc 643 . . . . . . . . . . 11 CovMap
1514adantr 452 . . . . . . . . . 10 CovMap
16 inopn 16964 . . . . . . . . . 10
176, 10, 15, 16syl3anc 1184 . . . . . . . . 9 CovMap
18 eqid 2435 . . . . . . . . 9
1917, 18fmptd 5885 . . . . . . . 8 CovMap
20 frn 5589 . . . . . . . 8
2119, 20syl 16 . . . . . . 7 CovMap
227cvmsn0 24947 . . . . . . . . 9
2322adantl 453 . . . . . . . 8 CovMap
24 dmmptg 5359 . . . . . . . . . . . 12
25 inex1g 4338 . . . . . . . . . . . 12
2624, 25mprg 2767 . . . . . . . . . . 11
2726eqeq1i 2442 . . . . . . . . . 10
28 dm0rn0 5078 . . . . . . . . . 10
2927, 28bitr3i 243 . . . . . . . . 9
3029necon3bii 2630 . . . . . . . 8
3123, 30sylib 189 . . . . . . 7 CovMap
3221, 31jca 519 . . . . . 6 CovMap
33 inss2 3554 . . . . . . . . . . . 12
34 elpw2g 4355 . . . . . . . . . . . . 13
3515, 34syl 16 . . . . . . . . . . . 12 CovMap
3633, 35mpbiri 225 . . . . . . . . . . 11 CovMap
3736, 18fmptd 5885 . . . . . . . . . 10 CovMap
38 frn 5589 . . . . . . . . . 10
3937, 38syl 16 . . . . . . . . 9 CovMap
40 sspwuni 4168 . . . . . . . . 9
4139, 40sylib 189 . . . . . . . 8 CovMap
42 simpl3 962 . . . . . . . . . . . . . 14 CovMap
43 imass2 5232 . . . . . . . . . . . . . 14
4442, 43syl 16 . . . . . . . . . . . . 13 CovMap
457cvmsuni 24948 . . . . . . . . . . . . . 14
4645adantl 453 . . . . . . . . . . . . 13 CovMap
4744, 46sseqtr4d 3377 . . . . . . . . . . . 12 CovMap
4847sselda 3340 . . . . . . . . . . 11 CovMap
49 eqid 2435 . . . . . . . . . . . . . . . . 17
50 ineq1 3527 . . . . . . . . . . . . . . . . . . 19
5150eqeq2d 2446 . . . . . . . . . . . . . . . . . 18
5251rspcev 3044 . . . . . . . . . . . . . . . . 17
5349, 52mpan2 653 . . . . . . . . . . . . . . . 16
5453ad2antrl 709 . . . . . . . . . . . . . . 15 CovMap
55 vex 2951 . . . . . . . . . . . . . . . . 17
5655inex1 4336 . . . . . . . . . . . . . . . 16
5718elrnmpt 5109 . . . . . . . . . . . . . . . 16
5856, 57ax-mp 8 . . . . . . . . . . . . . . 15
5954, 58sylibr 204 . . . . . . . . . . . . . 14 CovMap
60 simprr 734 . . . . . . . . . . . . . . 15 CovMap
61 simplr 732 . . . . . . . . . . . . . . 15 CovMap
62 elin 3522 . . . . . . . . . . . . . . 15
6360, 61, 62sylanbrc 646 . . . . . . . . . . . . . 14 CovMap
64 eleq2 2496 . . . . . . . . . . . . . . 15
6564rspcev 3044 . . . . . . . . . . . . . 14
6659, 63, 65syl2anc 643 . . . . . . . . . . . . 13 CovMap
6766rexlimdvaa 2823 . . . . . . . . . . . 12 CovMap
68 eluni2 4011 . . . . . . . . . . . 12
69 eluni2 4011 . . . . . . . . . . . 12
7067, 68, 693imtr4g 262 . . . . . . . . . . 11 CovMap
7148, 70mpd 15 . . . . . . . . . 10 CovMap
7271ex 424 . . . . . . . . 9 CovMap
7372ssrdv 3346 . . . . . . . 8 CovMap
7441, 73eqssd 3357 . . . . . . 7 CovMap
75 eldifsn 3919 . . . . . . . . . . . 12
76 vex 2951 . . . . . . . . . . . . . . 15
7718elrnmpt 5109 . . . . . . . . . . . . . . 15
7876, 77ax-mp 8 . . . . . . . . . . . . . 14
7950equcoms 1693 . . . . . . . . . . . . . . . . . 18
8079necon3ai 2638 . . . . . . . . . . . . . . . . 17
81 simpllr 736 . . . . . . . . . . . . . . . . . . 19 CovMap
82 simplr 732 . . . . . . . . . . . . . . . . . . 19 CovMap
83 simpr 448 . . . . . . . . . . . . . . . . . . 19 CovMap
847cvmsdisj 24949 . . . . . . . . . . . . . . . . . . 19
8581, 82, 83, 84syl3anc 1184 . . . . . . . . . . . . . . . . . 18 CovMap
8685ord 367 . . . . . . . . . . . . . . . . 17 CovMap
87 inss1 3553 . . . . . . . . . . . . . . . . . 18
88 sseq0 3651 . . . . . . . . . . . . . . . . . 18
8987, 88mpan 652 . . . . . . . . . . . . . . . . 17
9080, 86, 89syl56 32 . . . . . . . . . . . . . . . 16 CovMap
91 neeq1 2606 . . . . . . . . . . . . . . . . 17
92 ineq2 3528 . . . . . . . . . . . . . . . . . . 19
93 inindir 3551 . . . . . . . . . . . . . . . . . . 19
9492, 93syl6eqr 2485 . . . . . . . . . . . . . . . . . 18
9594eqeq1d 2443 . . . . . . . . . . . . . . . . 17
9691, 95imbi12d 312 . . . . . . . . . . . . . . . 16
9790, 96syl5ibrcom 214 . . . . . . . . . . . . . . 15 CovMap
9897rexlimdva 2822 . . . . . . . . . . . . . 14 CovMap
9978, 98syl5bi 209 . . . . . . . . . . . . 13 CovMap
10099imp3a 421 . . . . . . . . . . . 12 CovMap
10175, 100syl5bi 209 . . . . . . . . . . 11 CovMap
102101ralrimiv 2780 . . . . . . . . . 10 CovMap
103 inss1 3553 . . . . . . . . . . . . 13
104 resabs1 5167 . . . . . . . . . . . . 13
105103, 104ax-mp 8 . . . . . . . . . . . 12
1067cvmshmeo 24950 . . . . . . . . . . . . . 14 t t
107106adantll 695 . . . . . . . . . . . . 13 CovMap t t
1085adantr 452 . . . . . . . . . . . . . . 15 CovMap
1099sselda 3340 . . . . . . . . . . . . . . . 16 CovMap
110 elssuni 4035 . . . . . . . . . . . . . . . 16
111109, 110syl 16 . . . . . . . . . . . . . . 15 CovMap
112 eqid 2435 . . . . . . . . . . . . . . . 16
113112restuni 17218 . . . . . . . . . . . . . . 15 t
114108, 111, 113syl2anc 643 . . . . . . . . . . . . . 14 CovMap t
115103, 114syl5sseq 3388 . . . . . . . . . . . . 13 CovMap t
116 eqid 2435 . . . . . . . . . . . . . 14 t t
117116hmeores 17795 . . . . . . . . . . . . 13 t t t t t t t
118107, 115, 117syl2anc 643 . . . . . . . . . . . 12 CovMap t t t t
119105, 118syl5eqelr 2520 . . . . . . . . . . 11 CovMap t t t t
120103a1i 11 . . . . . . . . . . . . 13 CovMap
121 simpr 448 . . . . . . . . . . . . 13 CovMap
122 restabs 17221 . . . . . . . . . . . . 13 t t t
123108, 120, 121, 122syl3anc 1184 . . . . . . . . . . . 12 CovMap t t t
124 incom 3525 . . . . . . . . . . . . . . . . 17
125 cnvresima 5351 . . . . . . . . . . . . . . . . 17
126124, 125eqtr4i 2458 . . . . . . . . . . . . . . . 16
127126imaeq2i 5193 . . . . . . . . . . . . . . 15
1283adantr 452 . . . . . . . . . . . . . . . . . 18 CovMap CovMap
129 simplr 732 . . . . . . . . . . . . . . . . . 18 CovMap
1307cvmsf1o 24951 . . . . . . . . . . . . . . . . . 18 CovMap
131128, 129, 121, 130syl3anc 1184 . . . . . . . . . . . . . . . . 17 CovMap
132 f1ofo 5673 . . . . . . . . . . . . . . . . 17
133131, 132syl 16 . . . . . . . . . . . . . . . 16 CovMap
13442adantr 452 . . . . . . . . . . . . . . . 16 CovMap
135 foimacnv 5684 . . . . . . . . . . . . . . . 16
136133, 134, 135syl2anc 643 . . . . . . . . . . . . . . 15 CovMap
137127, 136syl5eq 2479 . . . . . . . . . . . . . 14 CovMap
138137oveq2d 6089 . . . . . . . . . . . . 13 CovMap t t t t
139 cvmtop2 24940 . . . . . . . . . . . . . . . 16 CovMap
1403, 139syl 16 . . . . . . . . . . . . . . 15 CovMap
1417cvmsrcl 24943 . . . . . . . . . . . . . . . 16
142141adantl 453 . . . . . . . . . . . . . . 15 CovMap
143 restabs 17221 . . . . . . . . . . . . . . 15 t t t
144140, 42, 142, 143syl3anc 1184 . . . . . . . . . . . . . 14 CovMap t t t
145144adantr 452 . . . . . . . . . . . . 13 CovMap t t t
146138, 145eqtrd 2467 . . . . . . . . . . . 12 CovMap t t t
147123, 146oveq12d 6091 . . . . . . . . . . 11 CovMap t t t t t t
148119, 147eleqtrd 2511 . . . . . . . . . 10 CovMap t t
149102, 148jca 519 . . . . . . . . 9 CovMap t t
150149ralrimiva 2781 . . . . . . . 8 CovMap t t
15156rgenw 2765 . . . . . . . . 9
15250cbvmptv 4292 . . . . . . . . . 10
153 sneq 3817 . . . . . . . . . . . . 13
154153difeq2d 3457 . . . . . . . . . . . 12
155 ineq1 3527 . . . . . . . . . . . . 13
156155eqeq1d 2443 . . . . . . . . . . . 12
157154, 156raleqbidv 2908 . . . . . . . . . . 11
158 reseq2 5133 . . . . . . . . . . . 12
159 oveq2 6081 . . . . . . . . . . . . 13 t t
160159oveq1d 6088 . . . . . . . . . . . 12 t t t t
161158, 160eleq12d 2503 . . . . . . . . . . 11 t t t t
162157, 161anbi12d 692 . . . . . . . . . 10 t t t t
163152, 162ralrnmpt 5870 . . . . . . . . 9 t t t t
164151, 163ax-mp 8 . . . . . . . 8 t t t t
165150, 164sylibr 204 . . . . . . 7 CovMap t t
16674, 165jca 519 . . . . . 6 CovMap t t
1677cvmscbv 24937 . . . . . . . 8 t t
168167cvmsval 24945 . . . . . . 7 t t
1695, 168syl 16 . . . . . 6 CovMap t t
1702, 32, 166, 169mpbir3and 1137 . . . . 5 CovMap
171 ne0i 3626 . . . . 5
172170, 171syl 16 . . . 4 CovMap
173172ex 424 . . 3 CovMap
174173exlimdv 1646 . 2 CovMap
1751, 174syl5bi 209 1 CovMap
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   w3a 936  wex 1550   wceq 1652   wcel 1725   wne 2598  wral 2697  wrex 2698  crab 2701  cvv 2948   cdif 3309   cin 3311   wss 3312  c0 3620  cpw 3791  csn 3806  cuni 4007   cmpt 4258  ccnv 4869   cdm 4870   crn 4871   cres 4872  cima 4873  wf 5442  wfo 5444  wf1o 5445  cfv 5446  (class class class)co 6073   ↾t crest 13640  ctop 16950   ccn 17280   chmeo 17777   CovMap ccvm 24934 This theorem is referenced by:  cvmcov2  24954 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-recs 6625  df-rdg 6660  df-oadd 6720  df-er 6897  df-map 7012  df-en 7102  df-fin 7105  df-fi 7408  df-rest 13642  df-topgen 13659  df-top 16955  df-bases 16957  df-topon 16958  df-cn 17283  df-hmeo 17779  df-cvm 24935
 Copyright terms: Public domain W3C validator