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

Theorem resttopon 17213
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 16979 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  J  e.  Top )
21adantr 452 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  J  e.  Top )
3 id 20 . . . 4  |-  ( A 
C_  X  ->  A  C_  X )
4 toponmax 16981 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  X  e.  J )
5 ssexg 4341 . . . 4  |-  ( ( A  C_  X  /\  X  e.  J )  ->  A  e.  _V )
63, 4, 5syl2anr 465 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  e.  _V )
7 resttop 17212 . . 3  |-  ( ( J  e.  Top  /\  A  e.  _V )  ->  ( Jt  A )  e.  Top )
82, 6, 7syl2anc 643 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  e.  Top )
9 simpr 448 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  C_  X )
10 dfss1 3537 . . . . . 6  |-  ( A 
C_  X  <->  ( X  i^i  A )  =  A )
119, 10sylib 189 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( X  i^i  A )  =  A )
12 simpl 444 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  J  e.  (TopOn `  X )
)
134adantr 452 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  X  e.  J )
14 elrestr 13644 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  e.  _V  /\  X  e.  J )  ->  ( X  i^i  A )  e.  ( Jt  A ) )
1512, 6, 13, 14syl3anc 1184 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( X  i^i  A )  e.  ( Jt  A ) )
1611, 15eqeltrrd 2510 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  e.  ( Jt  A ) )
17 elssuni 4035 . . . 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 13642 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  e.  _V )  ->  ( Jt  A )  =  ran  ( x  e.  J  |->  ( x  i^i  A
) ) )
206, 19syldan 457 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  =  ran  ( x  e.  J  |->  ( x  i^i  A
) ) )
21 inss2 3554 . . . . . . . . 9  |-  ( x  i^i  A )  C_  A
22 vex 2951 . . . . . . . . . . 11  |-  x  e. 
_V
2322inex1 4336 . . . . . . . . . 10  |-  ( x  i^i  A )  e. 
_V
2423elpw 3797 . . . . . . . . 9  |-  ( ( x  i^i  A )  e.  ~P A  <->  ( x  i^i  A )  C_  A
)
2521, 24mpbir 201 . . . . . . . 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 2435 . . . . . . 7  |-  ( x  e.  J  |->  ( x  i^i  A ) )  =  ( x  e.  J  |->  ( x  i^i 
A ) )
2826, 27fmptd 5884 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  (
x  e.  J  |->  ( x  i^i  A ) ) : J --> ~P A
)
29 frn 5588 . . . . . 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 3374 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  C_  ~P A )
32 sspwuni 4168 . . . 4  |-  ( ( Jt  A )  C_  ~P A 
<-> 
U. ( Jt  A ) 
C_  A )
3331, 32sylib 189 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  U. ( Jt  A )  C_  A
)
3418, 33eqssd 3357 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  =  U. ( Jt  A ) )
35 istopon 16978 . 2  |-  ( ( Jt  A )  e.  (TopOn `  A )  <->  ( ( Jt  A )  e.  Top  /\  A  =  U. ( Jt  A ) ) )
368, 34, 35sylanbrc 646 1  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  e.  (TopOn `  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725   _Vcvv 2948    i^i cin 3311    C_ wss 3312   ~Pcpw 3791   U.cuni 4007    e. cmpt 4258   ran crn 4870   -->wf 5441   ` cfv 5445  (class class class)co 6072   ↾t crest 13636   Topctop 16946  TopOnctopon 16947
This theorem is referenced by:  restuni  17214  stoig  17215  restsn2  17223  restlp  17235  restperf  17236  perfopn  17237  cnrest  17337  cnrest2  17338  cnrest2r  17339  cnpresti  17340  cnprest  17341  cnprest2  17342  restcnrm  17414  consuba  17471  kgentopon  17558  1stckgenlem  17573  kgen2ss  17575  kgencn  17576  xkoinjcn  17707  qtoprest  17737  flimrest  18003  fclsrest  18044  symgtgp  18119  dvrcn  18201  sszcld  18836  divcn  18886  cncfmptc  18929  cncfmptid  18930  cncfmpt2f  18932  cdivcncf  18935  cnmpt2pc  18941  icchmeo  18954  htpycc  18993  pcocn  19030  pcohtpylem  19032  pcopt  19035  pcopt2  19036  pcoass  19037  pcorevlem  19039  relcmpcmet  19257  limcvallem  19746  ellimc2  19752  limcres  19761  cnplimc  19762  cnlimc  19763  limccnp  19766  limccnp2  19767  dvbss  19776  perfdvf  19778  dvreslem  19784  dvres2lem  19785  dvcnp2  19794  dvcn  19795  dvaddbr  19812  dvmulbr  19813  dvcmulf  19819  dvmptres2  19836  dvmptcmul  19838  dvmptntr  19845  dvmptfsum  19847  dvcnvlem  19848  dvcnv  19849  lhop1lem  19885  lhop2  19887  lhop  19888  dvcnvrelem2  19890  dvcnvre  19891  ftc1lem3  19910  ftc1cn  19915  taylthlem1  20277  ulmdvlem3  20306  psercn  20330  abelth  20345  logcn  20526  cxpcn  20617  cxpcn2  20618  cxpcn3  20620  resqrcn  20621  sqrcn  20622  loglesqr  20630  xrlimcnp  20795  efrlim  20796  ftalem3  20845  xrge0pluscn  24314  xrge0mulc1cn  24315  lmlimxrge0  24322  pnfneige0  24324  lmxrge0  24325  esumcvg  24464  cvxpcon  24917  cvxscon  24918  cvmsf1o  24947  cvmliftlem8  24967  cvmlift2lem9a  24978  cvmlift2lem11  24988  cvmlift3lem6  24999  cnambfre  26201  ftc1cnnc  26225  areacirclem4  26230  areacirclem5  26232  ivthALT  26275
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4837  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-oprab 6076  df-mpt2 6077  df-1st 6340  df-2nd 6341  df-recs 6624  df-rdg 6659  df-oadd 6719  df-er 6896  df-en 7101  df-fin 7104  df-fi 7407  df-rest 13638  df-topgen 13655  df-top 16951  df-bases 16953  df-topon 16954
  Copyright terms: Public domain W3C validator