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

Theorem toponuni 19211
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 19209 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simprbi 464 1  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767   U.cuni 4245   ` cfv 5587   Topctop 19177  TopOnctopon 19178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-iota 5550  df-fun 5589  df-fv 5595  df-topon 19185
This theorem is referenced by:  toponmax  19212  toponss  19213  toponcom  19214  toponunii  19216  topgele  19218  topontopn  19226  toponmre  19376  cldmreon  19377  restuni  19445  resttopon2  19451  restlp  19466  restperf  19467  perfopn  19468  ordtcld1  19480  ordtcld2  19481  lmfval  19515  cnfval  19516  cnpfval  19517  cnpf2  19533  cnprcl2  19534  ssidcn  19538  iscnp4  19546  iscncl  19552  cncls2  19556  cncls  19557  cnntr  19558  cncnp  19563  lmcls  19585  lmcld  19586  iscnrm2  19621  ist0-2  19627  ist1-2  19630  ishaus2  19634  isreg2  19660  ordtt1  19662  sscmp  19687  dfcon2  19702  clscon  19713  concompcld  19717  1stccnp  19745  kgenval  19787  kgenuni  19791  1stckgenlem  19805  kgen2ss  19807  kgencn2  19809  txtopon  19843  txuni  19844  pttopon  19848  ptuniconst  19850  txcls  19856  ptclsg  19867  dfac14lem  19869  xkoccn  19871  ptcnplem  19873  ptcn  19879  cnmpt1t  19917  cnmpt2t  19925  cnmpt1res  19928  cnmpt2res  19929  cnmptkp  19932  cnmptk1p  19937  cnmptk2  19938  xkoinjcn  19939  elqtop3  19955  qtoptopon  19956  qtopcld  19965  qtoprest  19969  qtopcmap  19971  kqval  19978  kqcldsat  19985  isr0  19989  r0cld  19990  regr1lem  19991  kqnrmlem1  19995  kqnrmlem2  19996  pt1hmeo  20058  xpstopnlem1  20061  neifil  20132  trnei  20144  elflim  20223  flimss2  20224  flimss1  20225  flimopn  20227  fbflim2  20229  flimclslem  20236  flffval  20241  flfnei  20243  cnpflf2  20252  cnflf  20254  cnflf2  20255  isfcls2  20265  fclsopn  20266  fclsnei  20271  fclscmp  20282  ufilcmp  20284  fcfval  20285  fcfnei  20287  fcfelbas  20288  cnpfcf  20293  cnfcf  20294  alexsublem  20295  tmdcn2  20339  tmdgsum  20345  tmdgsum2  20346  symgtgp  20351  subgntr  20356  opnsubg  20357  clssubg  20358  clsnsg  20359  cldsubg  20360  tgpconcompeqg  20361  tgpconcomp  20362  ghmcnp  20364  snclseqg  20365  tgphaus  20366  tgpt1  20367  prdstmdd  20373  prdstgpd  20374  tsmsgsum  20388  tsmsid  20389  tsmsgsumOLD  20391  tsmsidOLD  20392  tsmsmhm  20399  tsmsadd  20400  tgptsmscld  20404  utop3cls  20505  mopnuni  20695  isxms2  20702  prdsxmslem2  20783  metdseq0  21109  cnmpt2pc  21179  ishtpy  21223  om1val  21281  pi1val  21288  csscld  21440  clsocv  21441  cfilfcls  21464  relcmpcmet  21506  limcres  22041  limccnp  22046  limccnp2  22047  dvbss  22056  perfdvf  22058  dvreslem  22064  dvres2lem  22065  dvcnp2  22074  dvaddbr  22092  dvmulbr  22093  dvcmulf  22099  dvmptres2  22116  dvmptcmul  22118  dvmptntr  22125  dvcnvrelem2  22170  ftc1cn  22195  taylthlem1  22518  ulmdvlem3  22547  efrlim  23043  pl1cn  27589  cvxpcon  28343  cvxscon  28344  ivthALT  29746  locfincf  29794  neibastop2  29798  neibastop3  29799  topmeet  29801  topjoin  29802  refsum2cnlem1  31006  unicntop  31029  dvresntr  31262  itgsubsticclem  31309  fourierdlem93  31516
  Copyright terms: Public domain W3C validator