MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resttopon Structured version   Visualization version   GIF version
Theorem resttopon 22672
Description: A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
resttopon ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐽 β†Ύt 𝐴) ∈ (TopOnβ€˜π΄))
Proof of Theorem resttopon
Dummy variable π‘₯ is distinct from all other variables.
StepHypRef Expression
1 topontop 22422 . . 3 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
2 id 22 . . . 4 (𝐴 βŠ† 𝑋 β†’ 𝐴 βŠ† 𝑋)
3 toponmax 22435 . . . 4 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 ∈ 𝐽)
4 ssexg 5323 . . . 4 ((𝐴 βŠ† 𝑋 ∧ 𝑋 ∈ 𝐽) β†’ 𝐴 ∈ V)
52, 3, 4syl2anr 597 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 ∈ V)
6 resttop 22671 . . 3 ((𝐽 ∈ Top ∧ 𝐴 ∈ V) β†’ (𝐽 β†Ύt 𝐴) ∈ Top)
71, 5, 6syl2an2r 683 . 2 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐽 β†Ύt 𝐴) ∈ Top)
8 simpr 485 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 βŠ† 𝑋)
9 sseqin2 4215 . . . . . 6 (𝐴 βŠ† 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
108, 9sylib 217 . . . . 5 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝑋 ∩ 𝐴) = 𝐴)
11 simpl 483 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
123adantr 481 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝑋 ∈ 𝐽)
13 elrestr 17376 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐽) β†’ (𝑋 ∩ 𝐴) ∈ (𝐽 β†Ύt 𝐴))
1411, 5, 12, 13syl3anc 1371 . . . . 5 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝑋 ∩ 𝐴) ∈ (𝐽 β†Ύt 𝐴))
1510, 14eqeltrrd 2834 . . . 4 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 ∈ (𝐽 β†Ύt 𝐴))
16 elssuni 4941 . . . 4 (𝐴 ∈ (𝐽 β†Ύt 𝐴) β†’ 𝐴 βŠ† βˆͺ (𝐽 β†Ύt 𝐴))
1715, 16syl 17 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 βŠ† βˆͺ (𝐽 β†Ύt 𝐴))
18 restval 17374 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 ∈ V) β†’ (𝐽 β†Ύt 𝐴) = ran (π‘₯ ∈ 𝐽 ↦ (π‘₯ ∩ 𝐴)))
195, 18syldan 591 . . . . 5 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐽 β†Ύt 𝐴) = ran (π‘₯ ∈ 𝐽 ↦ (π‘₯ ∩ 𝐴)))
20 inss2 4229 . . . . . . . . 9 (π‘₯ ∩ 𝐴) βŠ† 𝐴
21 vex 3478 . . . . . . . . . . 11 π‘₯ ∈ V
2221inex1 5317 . . . . . . . . . 10 (π‘₯ ∩ 𝐴) ∈ V
2322elpw 4606 . . . . . . . . 9 ((π‘₯ ∩ 𝐴) ∈ 𝒫 𝐴 ↔ (π‘₯ ∩ 𝐴) βŠ† 𝐴)
2420, 23mpbir 230 . . . . . . . 8 (π‘₯ ∩ 𝐴) ∈ 𝒫 𝐴
2524a1i 11 . . . . . . 7 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ π‘₯ ∈ 𝐽) β†’ (π‘₯ ∩ 𝐴) ∈ 𝒫 𝐴)
2625fmpttd 7116 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (π‘₯ ∈ 𝐽 ↦ (π‘₯ ∩ 𝐴)):π½βŸΆπ’« 𝐴)
2726frnd 6725 . . . . 5 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ran (π‘₯ ∈ 𝐽 ↦ (π‘₯ ∩ 𝐴)) βŠ† 𝒫 𝐴)
2819, 27eqsstrd 4020 . . . 4 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐽 β†Ύt 𝐴) βŠ† 𝒫 𝐴)
29 sspwuni 5103 . . . 4 ((𝐽 β†Ύt 𝐴) βŠ† 𝒫 𝐴 ↔ βˆͺ (𝐽 β†Ύt 𝐴) βŠ† 𝐴)
3028, 29sylib 217 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ βˆͺ (𝐽 β†Ύt 𝐴) βŠ† 𝐴)
3117, 30eqssd 3999 . 2 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 = βˆͺ (𝐽 β†Ύt 𝐴))
32 istopon 22421 . 2 ((𝐽 β†Ύt 𝐴) ∈ (TopOnβ€˜π΄) ↔ ((𝐽 β†Ύt 𝐴) ∈ Top ∧ 𝐴 = βˆͺ (𝐽 β†Ύt 𝐴)))
337, 31, 32sylanbrc 583 1 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐽 β†Ύt 𝐴) ∈ (TopOnβ€˜π΄))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3474   ∩ cin 3947   βŠ† wss 3948  π’« cpw 4602  βˆͺ cuni 4908   ↦ cmpt 5231  ran crn 5677  β€˜cfv 6543  (class class class)co 7411   β†Ύt crest 17368  Topctop 22402  TopOnctopon 22419
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-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  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-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  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-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-en 8942  df-fin 8945  df-fi 9408  df-rest 17370  df-topgen 17391  df-top 22403  df-topon 22420  df-bases 22456
This theorem is referenced by:  restuni  22673  stoig  22674  restsn2  22682  restlp  22694  restperf  22695  perfopn  22696  cnrest  22796  cnrest2  22797  cnrest2r  22798  cnpresti  22799  cnprest  22800  cnprest2  22801  restcnrm  22873  connsuba  22931  kgentopon  23049  1stckgenlem  23064  kgen2ss  23066  kgencn  23067  xkoinjcn  23198  qtoprest  23228  flimrest  23494  fclsrest  23535  flfcntr  23554  efmndtmd  23612  symgtgp  23617  dvrcn  23695  sszcld  24340  divcn  24391  cncfmptc  24435  cncfmptid  24436  cncfmpt2f  24438  cdivcncf  24444  cnmpopc  24451  icchmeo  24464  htpycc  24503  pcocn  24540  pcohtpylem  24542  pcopt  24545  pcopt2  24546  pcoass  24547  pcorevlem  24549  relcmpcmet  24842  limcvallem  25395  ellimc2  25401  limcres  25410  cnplimc  25411  cnlimc  25412  limccnp  25415  limccnp2  25416  dvbss  25425  perfdvf  25427  dvreslem  25433  dvres2lem  25434  dvcnp2  25444  dvcn  25445  dvaddbr  25462  dvmulbr  25463  dvcmulf  25469  dvmptres2  25486  dvmptcmul  25488  dvmptntr  25495  dvmptfsum  25499  dvcnvlem  25500  dvcnv  25501  lhop1lem  25537  lhop2  25539  lhop  25540  dvcnvrelem2  25542  dvcnvre  25543  ftc1lem3  25562  ftc1cn  25567  taylthlem1  25892  ulmdvlem3  25921  psercn  25945  abelth  25960  logcn  26162  cxpcn  26260  cxpcn2  26261  cxpcn3  26263  resqrtcn  26264  sqrtcn  26265  loglesqrt  26273  xrlimcnp  26480  efrlim  26481  ftalem3  26586  xrge0pluscn  32989  xrge0mulc1cn  32990  lmlimxrge0  32997  pnfneige0  33000  lmxrge0  33001  esumcvg  33153  cxpcncf1  33676  cvxpconn  34302  cvxsconn  34303  cvmsf1o  34332  cvmliftlem8  34352  cvmlift2lem9a  34363  cvmlift2lem11  34373  cvmlift3lem6  34384  gg-divcn  35232  gg-icchmeo  35239  gg-mulcncf  35242  gg-dvcnp2  35243  gg-dvmulbr  35244  gg-cxpcn  35253  ivthALT  35306  poimir  36607  broucube  36608  cnambfre  36622  ftc1cnnc  36646  areacirclem2  36663  areacirclem4  36665  fsumcncf  44673  ioccncflimc  44680  cncfuni  44681  icccncfext  44682  icocncflimc  44684  cncfiooicclem1  44688  cxpcncf2  44694  dvmptconst  44710  dvmptidg  44712  dvresntr  44713  itgsubsticclem  44770  dirkercncflem2  44899  dirkercncflem4  44901  fourierdlem32  44934  fourierdlem33  44935  fourierdlem62  44963  fourierdlem93  44994  fourierdlem101  45002
  Copyright terms: Public domain W3C validator