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

Theorem cvmsss2 30069
 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 3732 . 2
2 simpl2 1034 . . . . . 6 CovMap
3 simpl1 1033 . . . . . . . . . . . 12 CovMap CovMap
4 cvmtop1 30055 . . . . . . . . . . . 12 CovMap
53, 4syl 17 . . . . . . . . . . 11 CovMap
65adantr 472 . . . . . . . . . 10 CovMap
7 cvmcov.1 . . . . . . . . . . . . 13 t t
87cvmsss 30062 . . . . . . . . . . . 12
98adantl 473 . . . . . . . . . . 11 CovMap
109sselda 3418 . . . . . . . . . 10 CovMap
11 cvmcn 30057 . . . . . . . . . . . . 13 CovMap
123, 11syl 17 . . . . . . . . . . . 12 CovMap
13 cnima 20358 . . . . . . . . . . . 12
1412, 2, 13syl2anc 673 . . . . . . . . . . 11 CovMap
1514adantr 472 . . . . . . . . . 10 CovMap
16 inopn 20006 . . . . . . . . . 10
176, 10, 15, 16syl3anc 1292 . . . . . . . . 9 CovMap
18 eqid 2471 . . . . . . . . 9
1917, 18fmptd 6061 . . . . . . . 8 CovMap
20 frn 5747 . . . . . . . 8
2119, 20syl 17 . . . . . . 7 CovMap
227cvmsn0 30063 . . . . . . . . 9
2322adantl 473 . . . . . . . 8 CovMap
24 dmmptg 5339 . . . . . . . . . . . 12
25 inex1g 4539 . . . . . . . . . . . 12
2624, 25mprg 2770 . . . . . . . . . . 11
2726eqeq1i 2476 . . . . . . . . . 10
28 dm0rn0 5057 . . . . . . . . . 10
2927, 28bitr3i 259 . . . . . . . . 9
3029necon3bii 2695 . . . . . . . 8
3123, 30sylib 201 . . . . . . 7 CovMap
3221, 31jca 541 . . . . . 6 CovMap
33 inss2 3644 . . . . . . . . . . . 12
34 elpw2g 4564 . . . . . . . . . . . . 13
3515, 34syl 17 . . . . . . . . . . . 12 CovMap
3633, 35mpbiri 241 . . . . . . . . . . 11 CovMap
3736, 18fmptd 6061 . . . . . . . . . 10 CovMap
38 frn 5747 . . . . . . . . . 10
3937, 38syl 17 . . . . . . . . 9 CovMap
40 sspwuni 4360 . . . . . . . . 9
4139, 40sylib 201 . . . . . . . 8 CovMap
42 simpl3 1035 . . . . . . . . . . . . . 14 CovMap
43 imass2 5210 . . . . . . . . . . . . . 14
4442, 43syl 17 . . . . . . . . . . . . 13 CovMap
457cvmsuni 30064 . . . . . . . . . . . . . 14
4645adantl 473 . . . . . . . . . . . . 13 CovMap
4744, 46sseqtr4d 3455 . . . . . . . . . . . 12 CovMap
4847sselda 3418 . . . . . . . . . . 11 CovMap
49 eqid 2471 . . . . . . . . . . . . . . . . 17
50 ineq1 3618 . . . . . . . . . . . . . . . . . . 19
5150eqeq2d 2481 . . . . . . . . . . . . . . . . . 18
5251rspcev 3136 . . . . . . . . . . . . . . . . 17
5349, 52mpan2 685 . . . . . . . . . . . . . . . 16
5453ad2antrl 742 . . . . . . . . . . . . . . 15 CovMap
55 vex 3034 . . . . . . . . . . . . . . . . 17
5655inex1 4537 . . . . . . . . . . . . . . . 16
5718elrnmpt 5087 . . . . . . . . . . . . . . . 16
5856, 57ax-mp 5 . . . . . . . . . . . . . . 15
5954, 58sylibr 217 . . . . . . . . . . . . . 14 CovMap
60 simprr 774 . . . . . . . . . . . . . . 15 CovMap
61 simplr 770 . . . . . . . . . . . . . . 15 CovMap
6260, 61elind 3609 . . . . . . . . . . . . . 14 CovMap
63 eleq2 2538 . . . . . . . . . . . . . . 15
6463rspcev 3136 . . . . . . . . . . . . . 14
6559, 62, 64syl2anc 673 . . . . . . . . . . . . 13 CovMap
6665rexlimdvaa 2872 . . . . . . . . . . . 12 CovMap
67 eluni2 4194 . . . . . . . . . . . 12
68 eluni2 4194 . . . . . . . . . . . 12
6966, 67, 683imtr4g 278 . . . . . . . . . . 11 CovMap
7048, 69mpd 15 . . . . . . . . . 10 CovMap
7170ex 441 . . . . . . . . 9 CovMap
7271ssrdv 3424 . . . . . . . 8 CovMap
7341, 72eqssd 3435 . . . . . . 7 CovMap
74 eldifsn 4088 . . . . . . . . . . . 12
75 vex 3034 . . . . . . . . . . . . . . 15
7618elrnmpt 5087 . . . . . . . . . . . . . . 15
7775, 76ax-mp 5 . . . . . . . . . . . . . 14
7850equcoms 1872 . . . . . . . . . . . . . . . . . 18
7978necon3ai 2668 . . . . . . . . . . . . . . . . 17
80 simpllr 777 . . . . . . . . . . . . . . . . . . 19 CovMap
81 simplr 770 . . . . . . . . . . . . . . . . . . 19 CovMap
82 simpr 468 . . . . . . . . . . . . . . . . . . 19 CovMap
837cvmsdisj 30065 . . . . . . . . . . . . . . . . . . 19
8480, 81, 82, 83syl3anc 1292 . . . . . . . . . . . . . . . . . 18 CovMap
8584ord 384 . . . . . . . . . . . . . . . . 17 CovMap
86 inss1 3643 . . . . . . . . . . . . . . . . . 18
87 sseq0 3769 . . . . . . . . . . . . . . . . . 18
8886, 87mpan 684 . . . . . . . . . . . . . . . . 17
8979, 85, 88syl56 34 . . . . . . . . . . . . . . . 16 CovMap
90 neeq1 2705 . . . . . . . . . . . . . . . . 17
91 ineq2 3619 . . . . . . . . . . . . . . . . . . 19
92 inindir 3641 . . . . . . . . . . . . . . . . . . 19
9391, 92syl6eqr 2523 . . . . . . . . . . . . . . . . . 18
9493eqeq1d 2473 . . . . . . . . . . . . . . . . 17
9590, 94imbi12d 327 . . . . . . . . . . . . . . . 16
9689, 95syl5ibrcom 230 . . . . . . . . . . . . . . 15 CovMap
9796rexlimdva 2871 . . . . . . . . . . . . . 14 CovMap
9877, 97syl5bi 225 . . . . . . . . . . . . 13 CovMap
9998impd 438 . . . . . . . . . . . 12 CovMap
10074, 99syl5bi 225 . . . . . . . . . . 11 CovMap
101100ralrimiv 2808 . . . . . . . . . 10 CovMap
102 inss1 3643 . . . . . . . . . . . . 13
103 resabs1 5139 . . . . . . . . . . . . 13
104102, 103ax-mp 5 . . . . . . . . . . . 12
1057cvmshmeo 30066 . . . . . . . . . . . . . 14 t t
106105adantll 728 . . . . . . . . . . . . 13 CovMap t t
1075adantr 472 . . . . . . . . . . . . . . 15 CovMap
1089sselda 3418 . . . . . . . . . . . . . . . 16 CovMap
109 elssuni 4219 . . . . . . . . . . . . . . . 16
110108, 109syl 17 . . . . . . . . . . . . . . 15 CovMap
111 eqid 2471 . . . . . . . . . . . . . . . 16
112111restuni 20255 . . . . . . . . . . . . . . 15 t
113107, 110, 112syl2anc 673 . . . . . . . . . . . . . 14 CovMap t
114102, 113syl5sseq 3466 . . . . . . . . . . . . 13 CovMap t
115 eqid 2471 . . . . . . . . . . . . . 14 t t
116115hmeores 20863 . . . . . . . . . . . . 13 t t t t t t t
117106, 114, 116syl2anc 673 . . . . . . . . . . . 12 CovMap t t t t
118104, 117syl5eqelr 2554 . . . . . . . . . . 11 CovMap t t t t
119102a1i 11 . . . . . . . . . . . . 13 CovMap
120 simpr 468 . . . . . . . . . . . . 13 CovMap
121 restabs 20258 . . . . . . . . . . . . 13 t t t
122107, 119, 120, 121syl3anc 1292 . . . . . . . . . . . 12 CovMap t t t
123 incom 3616 . . . . . . . . . . . . . . . . 17
124 cnvresima 5331 . . . . . . . . . . . . . . . . 17
125123, 124eqtr4i 2496 . . . . . . . . . . . . . . . 16
126125imaeq2i 5172 . . . . . . . . . . . . . . 15
1273adantr 472 . . . . . . . . . . . . . . . . . 18 CovMap CovMap
128 simplr 770 . . . . . . . . . . . . . . . . . 18 CovMap
1297cvmsf1o 30067 . . . . . . . . . . . . . . . . . 18 CovMap
130127, 128, 120, 129syl3anc 1292 . . . . . . . . . . . . . . . . 17 CovMap
131 f1ofo 5835 . . . . . . . . . . . . . . . . 17
132130, 131syl 17 . . . . . . . . . . . . . . . 16 CovMap
13342adantr 472 . . . . . . . . . . . . . . . 16 CovMap
134 foimacnv 5845 . . . . . . . . . . . . . . . 16
135132, 133, 134syl2anc 673 . . . . . . . . . . . . . . 15 CovMap
136126, 135syl5eq 2517 . . . . . . . . . . . . . 14 CovMap
137136oveq2d 6324 . . . . . . . . . . . . 13 CovMap t t t t
138 cvmtop2 30056 . . . . . . . . . . . . . . . 16 CovMap
1393, 138syl 17 . . . . . . . . . . . . . . 15 CovMap
1407cvmsrcl 30059 . . . . . . . . . . . . . . . 16
141140adantl 473 . . . . . . . . . . . . . . 15 CovMap
142 restabs 20258 . . . . . . . . . . . . . . 15 t t t
143139, 42, 141, 142syl3anc 1292 . . . . . . . . . . . . . 14 CovMap t t t
144143adantr 472 . . . . . . . . . . . . 13 CovMap t t t
145137, 144eqtrd 2505 . . . . . . . . . . . 12 CovMap t t t
146122, 145oveq12d 6326 . . . . . . . . . . 11 CovMap t t t t t t
147118, 146eleqtrd 2551 . . . . . . . . . 10 CovMap t t
148101, 147jca 541 . . . . . . . . 9 CovMap t t
149148ralrimiva 2809 . . . . . . . 8 CovMap t t
15056rgenw 2768 . . . . . . . . 9
15150cbvmptv 4488 . . . . . . . . . 10
152 sneq 3969 . . . . . . . . . . . . 13
153152difeq2d 3540 . . . . . . . . . . . 12
154 ineq1 3618 . . . . . . . . . . . . 13
155154eqeq1d 2473 . . . . . . . . . . . 12
156153, 155raleqbidv 2987 . . . . . . . . . . 11
157 reseq2 5106 . . . . . . . . . . . 12
158 oveq2 6316 . . . . . . . . . . . . 13 t t
159158oveq1d 6323 . . . . . . . . . . . 12 t t t t
160157, 159eleq12d 2543 . . . . . . . . . . 11 t t t t
161156, 160anbi12d 725 . . . . . . . . . 10 t t t t
162151, 161ralrnmpt 6046 . . . . . . . . 9 t t t t
163150, 162ax-mp 5 . . . . . . . 8 t t t t
164149, 163sylibr 217 . . . . . . 7 CovMap t t
16573, 164jca 541 . . . . . 6 CovMap t t
1667cvmscbv 30053 . . . . . . . 8 t t
167166cvmsval 30061 . . . . . . 7 t t
1685, 167syl 17 . . . . . 6 CovMap t t
1692, 32, 165, 168mpbir3and 1213 . . . . 5 CovMap
170 ne0i 3728 . . . . 5
171169, 170syl 17 . . . 4 CovMap
172171ex 441 . . 3 CovMap
173172exlimdv 1787 . 2 CovMap
1741, 173syl5bi 225 1 CovMap
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   w3a 1007   wceq 1452  wex 1671   wcel 1904   wne 2641  wral 2756  wrex 2757  crab 2760  cvv 3031   cdif 3387   cin 3389   wss 3390  c0 3722  cpw 3942  csn 3959  cuni 4190   cmpt 4454  ccnv 4838   cdm 4839   crn 4840   cres 4841  cima 4842  wf 5585  wfo 5587  wf1o 5588  cfv 5589  (class class class)co 6308   ↾t crest 15397  ctop 19994   ccn 20317  chmeo 20845   CovMap ccvm 30050 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-oadd 7204  df-er 7381  df-map 7492  df-en 7588  df-fin 7591  df-fi 7943  df-rest 15399  df-topgen 15420  df-top 19998  df-bases 19999  df-topon 20000  df-cn 20320  df-hmeo 20847  df-cvm 30051 This theorem is referenced by:  cvmcov2  30070
 Copyright terms: Public domain W3C validator