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

Theorem resttopon 18787
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 18553 . . . 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 18555 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  X  e.  J )
5 ssexg 4459 . . . 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 18786 . . 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 3576 . . . . . 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 14388 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  e.  _V  /\  X  e.  J )  ->  ( X  i^i  A )  e.  ( Jt  A ) )
1512, 6, 13, 14syl3anc 1218 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( X  i^i  A )  e.  ( Jt  A ) )
1611, 15eqeltrrd 2518 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  e.  ( Jt  A ) )
17 elssuni 4142 . . . 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 14386 . . . . . 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 3592 . . . . . . . . 9  |-  ( x  i^i  A )  C_  A
22 vex 2996 . . . . . . . . . . 11  |-  x  e. 
_V
2322inex1 4454 . . . . . . . . . 10  |-  ( x  i^i  A )  e. 
_V
2423elpw 3887 . . . . . . . . 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 2443 . . . . . . 7  |-  ( x  e.  J  |->  ( x  i^i  A ) )  =  ( x  e.  J  |->  ( x  i^i 
A ) )
2826, 27fmptd 5888 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  (
x  e.  J  |->  ( x  i^i  A ) ) : J --> ~P A
)
29 frn 5586 . . . . . 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 3411 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  C_  ~P A )
32 sspwuni 4277 . . . 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 3394 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  A  =  U. ( Jt  A ) )
35 istopon 18552 . 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 1369    e. wcel 1756   _Vcvv 2993    i^i cin 3348    C_ wss 3349   ~Pcpw 3881   U.cuni 4112    e. cmpt 4371   ran crn 4862   -->wf 5435   ` cfv 5439  (class class class)co 6112   ↾t crest 14380   Topctop 18520  TopOnctopon 18521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-om 6498  df-1st 6598  df-2nd 6599  df-recs 6853  df-rdg 6887  df-oadd 6945  df-er 7122  df-en 7332  df-fin 7335  df-fi 7682  df-rest 14382  df-topgen 14403  df-top 18525  df-bases 18527  df-topon 18528
This theorem is referenced by:  restuni  18788  stoig  18789  restsn2  18797  restlp  18809  restperf  18810  perfopn  18811  cnrest  18911  cnrest2  18912  cnrest2r  18913  cnpresti  18914  cnprest  18915  cnprest2  18916  restcnrm  18988  consuba  19046  kgentopon  19133  1stckgenlem  19148  kgen2ss  19150  kgencn  19151  xkoinjcn  19282  qtoprest  19312  flimrest  19578  fclsrest  19619  symgtgp  19694  dvrcn  19780  sszcld  20416  divcn  20466  cncfmptc  20509  cncfmptid  20510  cncfmpt2f  20512  cdivcncf  20515  cnmpt2pc  20522  icchmeo  20535  htpycc  20574  pcocn  20611  pcohtpylem  20613  pcopt  20616  pcopt2  20617  pcoass  20618  pcorevlem  20620  relcmpcmet  20849  limcvallem  21368  ellimc2  21374  limcres  21383  cnplimc  21384  cnlimc  21385  limccnp  21388  limccnp2  21389  dvbss  21398  perfdvf  21400  dvreslem  21406  dvres2lem  21407  dvcnp2  21416  dvcn  21417  dvaddbr  21434  dvmulbr  21435  dvcmulf  21441  dvmptres2  21458  dvmptcmul  21460  dvmptntr  21467  dvmptfsum  21469  dvcnvlem  21470  dvcnv  21471  lhop1lem  21507  lhop2  21509  lhop  21510  dvcnvrelem2  21512  dvcnvre  21513  ftc1lem3  21532  ftc1cn  21537  taylthlem1  21860  ulmdvlem3  21889  psercn  21913  abelth  21928  logcn  22114  cxpcn  22205  cxpcn2  22206  cxpcn3  22208  resqrcn  22209  sqrcn  22210  loglesqr  22218  xrlimcnp  22384  efrlim  22385  ftalem3  22434  xrge0pluscn  26392  xrge0mulc1cn  26393  lmlimxrge0  26400  pnfneige0  26403  lmxrge0  26404  esumcvg  26557  cvxpcon  27153  cvxscon  27154  cvmsf1o  27183  cvmliftlem8  27203  cvmlift2lem9a  27214  cvmlift2lem11  27224  cvmlift3lem6  27235  cnambfre  28466  ftc1cnnc  28492  areacirclem2  28511  areacirclem4  28513  ivthALT  28556
  Copyright terms: Public domain W3C validator