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

Theorem resttopon 20163
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 19927 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  J  e.  Top )
21adantr 466 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  J  e.  Top )
3 id 23 . . . 4  |-  ( A 
C_  X  ->  A  C_  X )
4 toponmax 19929 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  X  e.  J )
5 ssexg 4566 . . . 4  |-  ( ( A  C_  X  /\  X  e.  J )  ->  A  e.  _V )
63, 4, 5syl2anr 480 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  e.  _V )
7 resttop 20162 . . 3  |-  ( ( J  e.  Top  /\  A  e.  _V )  ->  ( Jt  A )  e.  Top )
82, 6, 7syl2anc 665 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  e.  Top )
9 simpr 462 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  C_  X )
10 dfss1 3667 . . . . . 6  |-  ( A 
C_  X  <->  ( X  i^i  A )  =  A )
119, 10sylib 199 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( X  i^i  A )  =  A )
12 simpl 458 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  J  e.  (TopOn `  X )
)
134adantr 466 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  X  e.  J )
14 elrestr 15314 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  e.  _V  /\  X  e.  J )  ->  ( X  i^i  A )  e.  ( Jt  A ) )
1512, 6, 13, 14syl3anc 1264 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( X  i^i  A )  e.  ( Jt  A ) )
1611, 15eqeltrrd 2511 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  e.  ( Jt  A ) )
17 elssuni 4245 . . . 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 15312 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  e.  _V )  ->  ( Jt  A )  =  ran  ( x  e.  J  |->  ( x  i^i  A
) ) )
206, 19syldan 472 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  =  ran  ( x  e.  J  |->  ( x  i^i  A
) ) )
21 inss2 3683 . . . . . . . . 9  |-  ( x  i^i  A )  C_  A
22 vex 3084 . . . . . . . . . . 11  |-  x  e. 
_V
2322inex1 4561 . . . . . . . . . 10  |-  ( x  i^i  A )  e. 
_V
2423elpw 3985 . . . . . . . . 9  |-  ( ( x  i^i  A )  e.  ~P A  <->  ( x  i^i  A )  C_  A
)
2521, 24mpbir 212 . . . . . . . 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 2422 . . . . . . 7  |-  ( x  e.  J  |->  ( x  i^i  A ) )  =  ( x  e.  J  |->  ( x  i^i 
A ) )
2826, 27fmptd 6057 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  (
x  e.  J  |->  ( x  i^i  A ) ) : J --> ~P A
)
29 frn 5748 . . . . . 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 3498 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  C_  ~P A )
32 sspwuni 4385 . . . 4  |-  ( ( Jt  A )  C_  ~P A 
<-> 
U. ( Jt  A ) 
C_  A )
3331, 32sylib 199 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  U. ( Jt  A )  C_  A
)
3418, 33eqssd 3481 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  =  U. ( Jt  A ) )
35 istopon 19926 . 2  |-  ( ( Jt  A )  e.  (TopOn `  A )  <->  ( ( Jt  A )  e.  Top  /\  A  =  U. ( Jt  A ) ) )
368, 34, 35sylanbrc 668 1  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  e.  (TopOn `  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1868   _Vcvv 3081    i^i cin 3435    C_ wss 3436   ~Pcpw 3979   U.cuni 4216    |-> cmpt 4479   ran crn 4850   -->wf 5593   ` cfv 5597  (class class class)co 6301   ↾t crest 15306   Topctop 19903  TopOnctopon 19904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-1st 6803  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-oadd 7190  df-er 7367  df-en 7574  df-fin 7577  df-fi 7927  df-rest 15308  df-topgen 15329  df-top 19907  df-bases 19908  df-topon 19909
This theorem is referenced by:  restuni  20164  stoig  20165  restsn2  20173  restlp  20185  restperf  20186  perfopn  20187  cnrest  20287  cnrest2  20288  cnrest2r  20289  cnpresti  20290  cnprest  20291  cnprest2  20292  restcnrm  20364  consuba  20421  kgentopon  20539  1stckgenlem  20554  kgen2ss  20556  kgencn  20557  xkoinjcn  20688  qtoprest  20718  flimrest  20984  fclsrest  21025  flfcntr  21044  symgtgp  21102  dvrcn  21184  sszcld  21821  divcn  21886  cncfmptc  21929  cncfmptid  21930  cncfmpt2f  21932  cdivcncf  21935  cnmpt2pc  21942  icchmeo  21955  htpycc  21997  pcocn  22034  pcohtpylem  22036  pcopt  22039  pcopt2  22040  pcoass  22041  pcorevlem  22043  relcmpcmet  22272  limcvallem  22812  ellimc2  22818  limcres  22827  cnplimc  22828  cnlimc  22829  limccnp  22832  limccnp2  22833  dvbss  22842  perfdvf  22844  dvreslem  22850  dvres2lem  22851  dvcnp2  22860  dvcn  22861  dvaddbr  22878  dvmulbr  22879  dvcmulf  22885  dvmptres2  22902  dvmptcmul  22904  dvmptntr  22911  dvmptfsum  22913  dvcnvlem  22914  dvcnv  22915  lhop1lem  22951  lhop2  22953  lhop  22954  dvcnvrelem2  22956  dvcnvre  22957  ftc1lem3  22976  ftc1cn  22981  taylthlem1  23314  ulmdvlem3  23343  psercn  23367  abelth  23382  logcn  23578  cxpcn  23671  cxpcn2  23672  cxpcn3  23674  resqrtcn  23675  sqrtcn  23676  loglesqrt  23684  xrlimcnp  23880  efrlim  23881  ftalem3  23985  xrge0pluscn  28741  xrge0mulc1cn  28742  lmlimxrge0  28749  pnfneige0  28752  lmxrge0  28753  esumcvg  28902  cvxpcon  29960  cvxscon  29961  cvmsf1o  29990  cvmliftlem8  30010  cvmlift2lem9a  30021  cvmlift2lem11  30031  cvmlift3lem6  30042  ivthALT  30983  poimir  31886  broucube  31887  cnambfre  31902  ftc1cnnc  31929  areacirclem2  31946  areacirclem4  31948  fsumcncf  37574  ioccncflimc  37582  cncfuni  37583  icccncfext  37584  icocncflimc  37586  cncfiooicclem1  37590  cxpcncf2  37597  dvmptconst  37604  dvmptidg  37606  dvresntr  37607  itgsubsticclem  37671  dirkercncflem2  37785  dirkercncflem4  37787  fourierdlem32  37821  fourierdlem33  37822  fourierdlem62  37851  fourierdlem93  37882  fourierdlem101  37890
  Copyright terms: Public domain W3C validator