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

Theorem resttopon 20226
Description: A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
resttopon  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  e.  (TopOn `  A ) )

Proof of Theorem resttopon
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 topontop 19990 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  J  e.  Top )
21adantr 471 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  J  e.  Top )
3 id 22 . . . 4  |-  ( A 
C_  X  ->  A  C_  X )
4 toponmax 19992 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  X  e.  J )
5 ssexg 4563 . . . 4  |-  ( ( A  C_  X  /\  X  e.  J )  ->  A  e.  _V )
63, 4, 5syl2anr 485 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  e.  _V )
7 resttop 20225 . . 3  |-  ( ( J  e.  Top  /\  A  e.  _V )  ->  ( Jt  A )  e.  Top )
82, 6, 7syl2anc 671 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  e.  Top )
9 simpr 467 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  C_  X )
10 dfss1 3649 . . . . . 6  |-  ( A 
C_  X  <->  ( X  i^i  A )  =  A )
119, 10sylib 201 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( X  i^i  A )  =  A )
12 simpl 463 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  J  e.  (TopOn `  X )
)
134adantr 471 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  X  e.  J )
14 elrestr 15376 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  e.  _V  /\  X  e.  J )  ->  ( X  i^i  A )  e.  ( Jt  A ) )
1512, 6, 13, 14syl3anc 1276 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( X  i^i  A )  e.  ( Jt  A ) )
1611, 15eqeltrrd 2541 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  e.  ( Jt  A ) )
17 elssuni 4241 . . . 4  |-  ( A  e.  ( Jt  A )  ->  A  C_  U. ( Jt  A ) )
1816, 17syl 17 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  C_ 
U. ( Jt  A ) )
19 restval 15374 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  e.  _V )  ->  ( Jt  A )  =  ran  ( x  e.  J  |->  ( x  i^i  A
) ) )
206, 19syldan 477 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  =  ran  ( x  e.  J  |->  ( x  i^i  A
) ) )
21 inss2 3665 . . . . . . . . 9  |-  ( x  i^i  A )  C_  A
22 vex 3060 . . . . . . . . . . 11  |-  x  e. 
_V
2322inex1 4558 . . . . . . . . . 10  |-  ( x  i^i  A )  e. 
_V
2423elpw 3969 . . . . . . . . 9  |-  ( ( x  i^i  A )  e.  ~P A  <->  ( x  i^i  A )  C_  A
)
2521, 24mpbir 214 . . . . . . . 8  |-  ( x  i^i  A )  e. 
~P A
2625a1i 11 . . . . . . 7  |-  ( ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  /\  x  e.  J )  ->  (
x  i^i  A )  e.  ~P A )
27 eqid 2462 . . . . . . 7  |-  ( x  e.  J  |->  ( x  i^i  A ) )  =  ( x  e.  J  |->  ( x  i^i 
A ) )
2826, 27fmptd 6069 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  (
x  e.  J  |->  ( x  i^i  A ) ) : J --> ~P A
)
29 frn 5758 . . . . . 6  |-  ( ( x  e.  J  |->  ( x  i^i  A ) ) : J --> ~P A  ->  ran  ( x  e.  J  |->  ( x  i^i 
A ) )  C_  ~P A )
3028, 29syl 17 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ran  ( x  e.  J  |->  ( x  i^i  A
) )  C_  ~P A )
3120, 30eqsstrd 3478 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  C_  ~P A )
32 sspwuni 4381 . . . 4  |-  ( ( Jt  A )  C_  ~P A 
<-> 
U. ( Jt  A ) 
C_  A )
3331, 32sylib 201 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  U. ( Jt  A )  C_  A
)
3418, 33eqssd 3461 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  =  U. ( Jt  A ) )
35 istopon 19989 . 2  |-  ( ( Jt  A )  e.  (TopOn `  A )  <->  ( ( Jt  A )  e.  Top  /\  A  =  U. ( Jt  A ) ) )
368, 34, 35sylanbrc 675 1  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  e.  (TopOn `  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1455    e. wcel 1898   _Vcvv 3057    i^i cin 3415    C_ wss 3416   ~Pcpw 3963   U.cuni 4212    |-> cmpt 4475   ran crn 4854   -->wf 5597   ` cfv 5601  (class class class)co 6315   ↾t crest 15368   Topctop 19966  TopOnctopon 19967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-oadd 7212  df-er 7389  df-en 7596  df-fin 7599  df-fi 7951  df-rest 15370  df-topgen 15391  df-top 19970  df-bases 19971  df-topon 19972
This theorem is referenced by:  restuni  20227  stoig  20228  restsn2  20236  restlp  20248  restperf  20249  perfopn  20250  cnrest  20350  cnrest2  20351  cnrest2r  20352  cnpresti  20353  cnprest  20354  cnprest2  20355  restcnrm  20427  consuba  20484  kgentopon  20602  1stckgenlem  20617  kgen2ss  20619  kgencn  20620  xkoinjcn  20751  qtoprest  20781  flimrest  21047  fclsrest  21088  flfcntr  21107  symgtgp  21165  dvrcn  21247  sszcld  21884  divcn  21949  cncfmptc  21992  cncfmptid  21993  cncfmpt2f  21995  cdivcncf  21998  cnmpt2pc  22005  icchmeo  22018  htpycc  22060  pcocn  22097  pcohtpylem  22099  pcopt  22102  pcopt2  22103  pcoass  22104  pcorevlem  22106  relcmpcmet  22335  limcvallem  22875  ellimc2  22881  limcres  22890  cnplimc  22891  cnlimc  22892  limccnp  22895  limccnp2  22896  dvbss  22905  perfdvf  22907  dvreslem  22913  dvres2lem  22914  dvcnp2  22923  dvcn  22924  dvaddbr  22941  dvmulbr  22942  dvcmulf  22948  dvmptres2  22965  dvmptcmul  22967  dvmptntr  22974  dvmptfsum  22976  dvcnvlem  22977  dvcnv  22978  lhop1lem  23014  lhop2  23016  lhop  23017  dvcnvrelem2  23019  dvcnvre  23020  ftc1lem3  23039  ftc1cn  23044  taylthlem1  23377  ulmdvlem3  23406  psercn  23430  abelth  23445  logcn  23641  cxpcn  23734  cxpcn2  23735  cxpcn3  23737  resqrtcn  23738  sqrtcn  23739  loglesqrt  23747  xrlimcnp  23943  efrlim  23944  ftalem3  24048  xrge0pluscn  28795  xrge0mulc1cn  28796  lmlimxrge0  28803  pnfneige0  28806  lmxrge0  28807  esumcvg  28956  cvxpcon  30014  cvxscon  30015  cvmsf1o  30044  cvmliftlem8  30064  cvmlift2lem9a  30075  cvmlift2lem11  30085  cvmlift3lem6  30096  ivthALT  31040  poimir  32018  broucube  32019  cnambfre  32034  ftc1cnnc  32061  areacirclem2  32078  areacirclem4  32080  fsumcncf  37793  ioccncflimc  37801  cncfuni  37802  icccncfext  37803  icocncflimc  37805  cncfiooicclem1  37809  cxpcncf2  37816  dvmptconst  37823  dvmptidg  37825  dvresntr  37826  itgsubsticclem  37890  dirkercncflem2  38004  dirkercncflem4  38006  fourierdlem32  38040  fourierdlem33  38041  fourierdlem62  38070  fourierdlem93  38101  fourierdlem101  38109
  Copyright terms: Public domain W3C validator