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

Theorem restuni 20155
Description: The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
Hypothesis
Ref Expression
restuni.1  |-  X  = 
U. J
Assertion
Ref Expression
restuni  |-  ( ( J  e.  Top  /\  A  C_  X )  ->  A  =  U. ( Jt  A ) )

Proof of Theorem restuni
StepHypRef Expression
1 restuni.1 . . . 4  |-  X  = 
U. J
21toptopon 19925 . . 3  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
3 resttopon 20154 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  A  C_  X )  ->  ( Jt  A )  e.  (TopOn `  A ) )
42, 3sylanb 474 . 2  |-  ( ( J  e.  Top  /\  A  C_  X )  -> 
( Jt  A )  e.  (TopOn `  A ) )
5 toponuni 19919 . 2  |-  ( ( Jt  A )  e.  (TopOn `  A )  ->  A  =  U. ( Jt  A ) )
64, 5syl 17 1  |-  ( ( J  e.  Top  /\  A  C_  X )  ->  A  =  U. ( Jt  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1867    C_ wss 3433   U.cuni 4213   ` cfv 5593  (class class class)co 6297   ↾t crest 15297   Topctop 19894  TopOnctopon 19895
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 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4530  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589
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 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-br 4418  df-opab 4477  df-mpt 4478  df-tr 4513  df-eprel 4757  df-id 4761  df-po 4767  df-so 4768  df-fr 4805  df-we 4807  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-pred 5391  df-ord 5437  df-on 5438  df-lim 5439  df-suc 5440  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6300  df-oprab 6301  df-mpt2 6302  df-om 6699  df-1st 6799  df-2nd 6800  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-oadd 7186  df-er 7363  df-en 7570  df-fin 7573  df-fi 7923  df-rest 15299  df-topgen 15320  df-top 19898  df-bases 19899  df-topon 19900
This theorem is referenced by:  restuni2  20160  restcld  20165  restopn2  20170  neitr  20173  restcls  20174  restntr  20175  rncmp  20388  cmpsublem  20391  cmpsub  20392  fiuncmp  20396  consubclo  20416  conima  20417  concn  20418  nllyrest  20478  cldllycmp  20487  lly1stc  20488  llycmpkgen2  20542  1stckgen  20546  txkgen  20644  xkopjcn  20648  xkococnlem  20651  cnextfres1  21060  cnextfres  21061  cncfcnvcn  21930  cnheibor  21960  evthicc  22387  psercn  23358  abelth  23373  conpcon  29947  cvmscld  29985  cvmsss2  29986  cvmliftmolem1  29993  cvmliftlem10  30006  cvmlift2lem9  30023  cvmlift2lem11  30025  cvmlift2lem12  30026  cvmlift3lem7  30037  ivthALT  30977  ptrest  31847  poimirlem29  31877  poimirlem30  31878  poimirlem31  31879  poimir  31881  cncfuni  37551  cncfiooicclem1  37558  stoweidlem28  37675  dirkercncflem4  37755  fourierdlem42  37799  fourierdlem42OLD  37800
  Copyright terms: Public domain W3C validator