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

Theorem toponuni 16997
Description: The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
toponuni  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )

Proof of Theorem toponuni
StepHypRef Expression
1 istopon 16995 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simprbi 452 1  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726   U.cuni 4017   ` cfv 5457   Topctop 16963  TopOnctopon 16964
This theorem is referenced by:  toponmax  16998  toponss  16999  toponcom  17000  toponunii  17002  topgele  17004  topontopn  17012  toponmre  17162  cldmreon  17163  restuni  17231  resttopon2  17237  restlp  17252  restperf  17253  perfopn  17254  ordtcld1  17266  ordtcld2  17267  lmfval  17301  cnfval  17302  cnpfval  17303  cnpf2  17319  cnprcl2  17320  ssidcn  17324  iscnp4  17332  iscncl  17338  cncls2  17342  cncls  17343  cnntr  17344  cncnp  17349  lmcls  17371  lmcld  17372  iscnrm2  17407  ist0-2  17413  ist1-2  17416  ishaus2  17420  isreg2  17446  ordtt1  17448  sscmp  17473  dfcon2  17487  clscon  17498  concompcld  17502  1stccnp  17530  kgenval  17572  kgenuni  17576  1stckgenlem  17590  kgen2ss  17592  kgencn2  17594  txtopon  17628  txuni  17629  pttopon  17633  ptuniconst  17635  txcls  17641  ptclsg  17652  dfac14lem  17654  xkoccn  17656  ptcnplem  17658  ptcn  17664  cnmpt1t  17702  cnmpt2t  17710  cnmpt1res  17713  cnmpt2res  17714  cnmptkp  17717  cnmptk1p  17722  cnmptk2  17723  xkoinjcn  17724  elqtop3  17740  qtoptopon  17741  qtopcld  17750  qtoprest  17754  qtopcmap  17756  kqval  17763  kqcldsat  17770  isr0  17774  r0cld  17775  regr1lem  17776  kqnrmlem1  17780  kqnrmlem2  17781  pt1hmeo  17843  xpstopnlem1  17846  neifil  17917  trnei  17929  elflim  18008  flimss2  18009  flimss1  18010  flimopn  18012  fbflim2  18014  flimclslem  18021  flffval  18026  flfnei  18028  cnpflf2  18037  cnflf  18039  cnflf2  18040  isfcls2  18050  fclsopn  18051  fclsnei  18056  fclscmp  18067  ufilcmp  18069  fcfval  18070  fcfnei  18072  fcfelbas  18073  cnpfcf  18078  cnfcf  18079  alexsublem  18080  tmdcn2  18124  tmdgsum  18130  tmdgsum2  18131  symgtgp  18136  subgntr  18141  opnsubg  18142  clssubg  18143  clsnsg  18144  cldsubg  18145  tgpconcompeqg  18146  tgpconcomp  18147  ghmcnp  18149  snclseqg  18150  tgphaus  18151  tgpt1  18152  prdstmdd  18158  prdstgpd  18159  tsmsgsum  18173  tsmsid  18174  tsmsmhm  18180  tsmsadd  18181  tgptsmscld  18185  utop3cls  18286  mopnuni  18476  isxms2  18483  prdsxmslem2  18564  metdseq0  18889  cnmpt2pc  18958  ishtpy  19002  om1val  19060  pi1val  19067  csscld  19208  clsocv  19209  cfilfcls  19232  relcmpcmet  19274  limcres  19778  limccnp  19783  limccnp2  19784  dvbss  19793  perfdvf  19795  dvreslem  19801  dvres2lem  19802  dvcnp2  19811  dvaddbr  19829  dvmulbr  19830  dvcmulf  19836  dvmptres2  19853  dvmptcmul  19855  dvmptntr  19862  dvcnvrelem2  19907  ftc1cn  19932  taylthlem1  20294  ulmdvlem3  20323  efrlim  20813  cvxpcon  24934  cvxscon  24935  ivthALT  26352  locfincf  26400  neibastop2  26404  neibastop3  26405  topmeet  26407  topjoin  26408  refsum2cnlem1  27698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-iota 5421  df-fun 5459  df-fv 5465  df-topon 16971
  Copyright terms: Public domain W3C validator