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

Theorem resttopon 19788
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 19553 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  J  e.  Top )
21adantr 465 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  J  e.  Top )
3 id 22 . . . 4  |-  ( A 
C_  X  ->  A  C_  X )
4 toponmax 19555 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  X  e.  J )
5 ssexg 4602 . . . 4  |-  ( ( A  C_  X  /\  X  e.  J )  ->  A  e.  _V )
63, 4, 5syl2anr 478 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  e.  _V )
7 resttop 19787 . . 3  |-  ( ( J  e.  Top  /\  A  e.  _V )  ->  ( Jt  A )  e.  Top )
82, 6, 7syl2anc 661 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  e.  Top )
9 simpr 461 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  C_  X )
10 dfss1 3699 . . . . . 6  |-  ( A 
C_  X  <->  ( X  i^i  A )  =  A )
119, 10sylib 196 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( X  i^i  A )  =  A )
12 simpl 457 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  J  e.  (TopOn `  X )
)
134adantr 465 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  X  e.  J )
14 elrestr 14845 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  e.  _V  /\  X  e.  J )  ->  ( X  i^i  A )  e.  ( Jt  A ) )
1512, 6, 13, 14syl3anc 1228 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( X  i^i  A )  e.  ( Jt  A ) )
1611, 15eqeltrrd 2546 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  e.  ( Jt  A ) )
17 elssuni 4281 . . . 4  |-  ( A  e.  ( Jt  A )  ->  A  C_  U. ( Jt  A ) )
1816, 17syl 16 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  C_ 
U. ( Jt  A ) )
19 restval 14843 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  e.  _V )  ->  ( Jt  A )  =  ran  ( x  e.  J  |->  ( x  i^i  A
) ) )
206, 19syldan 470 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  =  ran  ( x  e.  J  |->  ( x  i^i  A
) ) )
21 inss2 3715 . . . . . . . . 9  |-  ( x  i^i  A )  C_  A
22 vex 3112 . . . . . . . . . . 11  |-  x  e. 
_V
2322inex1 4597 . . . . . . . . . 10  |-  ( x  i^i  A )  e. 
_V
2423elpw 4021 . . . . . . . . 9  |-  ( ( x  i^i  A )  e.  ~P A  <->  ( x  i^i  A )  C_  A
)
2521, 24mpbir 209 . . . . . . . 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 2457 . . . . . . 7  |-  ( x  e.  J  |->  ( x  i^i  A ) )  =  ( x  e.  J  |->  ( x  i^i 
A ) )
2826, 27fmptd 6056 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  (
x  e.  J  |->  ( x  i^i  A ) ) : J --> ~P A
)
29 frn 5743 . . . . . 6  |-  ( ( x  e.  J  |->  ( x  i^i  A ) ) : J --> ~P A  ->  ran  ( x  e.  J  |->  ( x  i^i 
A ) )  C_  ~P A )
3028, 29syl 16 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ran  ( x  e.  J  |->  ( x  i^i  A
) )  C_  ~P A )
3120, 30eqsstrd 3533 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  C_  ~P A )
32 sspwuni 4421 . . . 4  |-  ( ( Jt  A )  C_  ~P A 
<-> 
U. ( Jt  A ) 
C_  A )
3331, 32sylib 196 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  U. ( Jt  A )  C_  A
)
3418, 33eqssd 3516 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  =  U. ( Jt  A ) )
35 istopon 19552 . 2  |-  ( ( Jt  A )  e.  (TopOn `  A )  <->  ( ( Jt  A )  e.  Top  /\  A  =  U. ( Jt  A ) ) )
368, 34, 35sylanbrc 664 1  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  e.  (TopOn `  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1395    e. wcel 1819   _Vcvv 3109    i^i cin 3470    C_ wss 3471   ~Pcpw 4015   U.cuni 4251    |-> cmpt 4515   ran crn 5009   -->wf 5590   ` cfv 5594  (class class class)co 6296   ↾t crest 14837   Topctop 19520  TopOnctopon 19521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-oadd 7152  df-er 7329  df-en 7536  df-fin 7539  df-fi 7889  df-rest 14839  df-topgen 14860  df-top 19525  df-bases 19527  df-topon 19528
This theorem is referenced by:  restuni  19789  stoig  19790  restsn2  19798  restlp  19810  restperf  19811  perfopn  19812  cnrest  19912  cnrest2  19913  cnrest2r  19914  cnpresti  19915  cnprest  19916  cnprest2  19917  restcnrm  19989  consuba  20046  kgentopon  20164  1stckgenlem  20179  kgen2ss  20181  kgencn  20182  xkoinjcn  20313  qtoprest  20343  flimrest  20609  fclsrest  20650  symgtgp  20725  dvrcn  20811  sszcld  21447  divcn  21497  cncfmptc  21540  cncfmptid  21541  cncfmpt2f  21543  cdivcncf  21546  cnmpt2pc  21553  icchmeo  21566  htpycc  21605  pcocn  21642  pcohtpylem  21644  pcopt  21647  pcopt2  21648  pcoass  21649  pcorevlem  21651  relcmpcmet  21880  limcvallem  22400  ellimc2  22406  limcres  22415  cnplimc  22416  cnlimc  22417  limccnp  22420  limccnp2  22421  dvbss  22430  perfdvf  22432  dvreslem  22438  dvres2lem  22439  dvcnp2  22448  dvcn  22449  dvaddbr  22466  dvmulbr  22467  dvcmulf  22473  dvmptres2  22490  dvmptcmul  22492  dvmptntr  22499  dvmptfsum  22501  dvcnvlem  22502  dvcnv  22503  lhop1lem  22539  lhop2  22541  lhop  22542  dvcnvrelem2  22544  dvcnvre  22545  ftc1lem3  22564  ftc1cn  22569  taylthlem1  22893  ulmdvlem3  22922  psercn  22946  abelth  22961  logcn  23153  cxpcn  23244  cxpcn2  23245  cxpcn3  23247  resqrtcn  23248  sqrtcn  23249  loglesqrt  23257  xrlimcnp  23423  efrlim  23424  ftalem3  23473  xrge0pluscn  28075  xrge0mulc1cn  28076  lmlimxrge0  28083  pnfneige0  28086  lmxrge0  28087  esumcvg  28248  cvxpcon  28862  cvxscon  28863  cvmsf1o  28892  cvmliftlem8  28912  cvmlift2lem9a  28923  cvmlift2lem11  28933  cvmlift3lem6  28944  cnambfre  30225  ftc1cnnc  30251  areacirclem2  30270  areacirclem4  30272  ivthALT  30315  fsumcncf  31841  ioccncflimc  31849  cncfuni  31850  icccncfext  31851  icocncflimc  31853  cncfiooicclem1  31857  cxpcncf2  31864  dvmptconst  31871  dvmptidg  31873  dvresntr  31874  itgsubsticclem  31935  dirkercncflem2  32047  dirkercncflem4  32049  fourierdlem32  32082  fourierdlem33  32083  fourierdlem62  32112  fourierdlem93  32143  fourierdlem101  32151
  Copyright terms: Public domain W3C validator