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

Theorem mreiincl 17542
Description: A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Assertion
Ref Expression
mreiincl ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ 𝐼 β‰  βˆ… ∧ βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢) β†’ ∩ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐢)
Distinct variable groups:   𝑦,𝐼   𝑦,𝑋   𝑦,𝐢
Allowed substitution hint:   𝑆(𝑦)

Proof of Theorem mreiincl
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 dfiin2g 5035 . . 3 (βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢 β†’ ∩ 𝑦 ∈ 𝐼 𝑆 = ∩ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆})
213ad2ant3 1135 . 2 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ 𝐼 β‰  βˆ… ∧ βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢) β†’ ∩ 𝑦 ∈ 𝐼 𝑆 = ∩ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆})
3 simp1 1136 . . 3 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ 𝐼 β‰  βˆ… ∧ βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢) β†’ 𝐢 ∈ (Mooreβ€˜π‘‹))
4 uniiunlem 4084 . . . . 5 (βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢 β†’ (βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢 ↔ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} βŠ† 𝐢))
54ibi 266 . . . 4 (βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢 β†’ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} βŠ† 𝐢)
653ad2ant3 1135 . . 3 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ 𝐼 β‰  βˆ… ∧ βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢) β†’ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} βŠ† 𝐢)
7 n0 4346 . . . . . 6 (𝐼 β‰  βˆ… ↔ βˆƒπ‘¦ 𝑦 ∈ 𝐼)
8 nfra1 3281 . . . . . . . 8 β„²π‘¦βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢
9 nfre1 3282 . . . . . . . . . 10 β„²π‘¦βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆
109nfab 2909 . . . . . . . . 9 Ⅎ𝑦{𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆}
11 nfcv 2903 . . . . . . . . 9 β„²π‘¦βˆ…
1210, 11nfne 3043 . . . . . . . 8 Ⅎ𝑦{𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} β‰  βˆ…
138, 12nfim 1899 . . . . . . 7 Ⅎ𝑦(βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢 β†’ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} β‰  βˆ…)
14 rsp 3244 . . . . . . . . . 10 (βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢 β†’ (𝑦 ∈ 𝐼 β†’ 𝑆 ∈ 𝐢))
1514com12 32 . . . . . . . . 9 (𝑦 ∈ 𝐼 β†’ (βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢 β†’ 𝑆 ∈ 𝐢))
16 elisset 2815 . . . . . . . . . . 11 (𝑆 ∈ 𝐢 β†’ βˆƒπ‘  𝑠 = 𝑆)
17 rspe 3246 . . . . . . . . . . . 12 ((𝑦 ∈ 𝐼 ∧ βˆƒπ‘  𝑠 = 𝑆) β†’ βˆƒπ‘¦ ∈ 𝐼 βˆƒπ‘  𝑠 = 𝑆)
1817ex 413 . . . . . . . . . . 11 (𝑦 ∈ 𝐼 β†’ (βˆƒπ‘  𝑠 = 𝑆 β†’ βˆƒπ‘¦ ∈ 𝐼 βˆƒπ‘  𝑠 = 𝑆))
1916, 18syl5 34 . . . . . . . . . 10 (𝑦 ∈ 𝐼 β†’ (𝑆 ∈ 𝐢 β†’ βˆƒπ‘¦ ∈ 𝐼 βˆƒπ‘  𝑠 = 𝑆))
20 rexcom4 3285 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐼 βˆƒπ‘  𝑠 = 𝑆 ↔ βˆƒπ‘ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆)
2119, 20imbitrdi 250 . . . . . . . . 9 (𝑦 ∈ 𝐼 β†’ (𝑆 ∈ 𝐢 β†’ βˆƒπ‘ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆))
2215, 21syld 47 . . . . . . . 8 (𝑦 ∈ 𝐼 β†’ (βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢 β†’ βˆƒπ‘ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆))
23 abn0 4380 . . . . . . . 8 ({𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} β‰  βˆ… ↔ βˆƒπ‘ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆)
2422, 23imbitrrdi 251 . . . . . . 7 (𝑦 ∈ 𝐼 β†’ (βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢 β†’ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} β‰  βˆ…))
2513, 24exlimi 2210 . . . . . 6 (βˆƒπ‘¦ 𝑦 ∈ 𝐼 β†’ (βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢 β†’ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} β‰  βˆ…))
267, 25sylbi 216 . . . . 5 (𝐼 β‰  βˆ… β†’ (βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢 β†’ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} β‰  βˆ…))
2726imp 407 . . . 4 ((𝐼 β‰  βˆ… ∧ βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢) β†’ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} β‰  βˆ…)
28273adant1 1130 . . 3 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ 𝐼 β‰  βˆ… ∧ βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢) β†’ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} β‰  βˆ…)
29 mreintcl 17541 . . 3 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} βŠ† 𝐢 ∧ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} β‰  βˆ…) β†’ ∩ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} ∈ 𝐢)
303, 6, 28, 29syl3anc 1371 . 2 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ 𝐼 β‰  βˆ… ∧ βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢) β†’ ∩ {𝑠 ∣ βˆƒπ‘¦ ∈ 𝐼 𝑠 = 𝑆} ∈ 𝐢)
312, 30eqeltrd 2833 1 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ 𝐼 β‰  βˆ… ∧ βˆ€π‘¦ ∈ 𝐼 𝑆 ∈ 𝐢) β†’ ∩ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐢)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ w3a 1087   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  {cab 2709   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070   βŠ† wss 3948  βˆ…c0 4322  βˆ© cint 4950  βˆ© ciin 4998  β€˜cfv 6543  Moorecmre 17528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-mre 17532
This theorem is referenced by:  mreriincl  17544  mretopd  22603
  Copyright terms: Public domain W3C validator