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

Theorem toponuni 19866
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 19864 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simprbi 465 1  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1867   U.cuni 4213   ` cfv 5592   Topctop 19841  TopOnctopon 19842
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-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  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-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-iota 5556  df-fun 5594  df-fv 5600  df-topon 19847
This theorem is referenced by:  toponmax  19867  toponss  19868  toponcom  19869  toponunii  19871  topgele  19873  topontopn  19881  toponmre  20033  cldmreon  20034  restuni  20102  resttopon2  20108  restlp  20123  restperf  20124  perfopn  20125  ordtcld1  20137  ordtcld2  20138  lmfval  20172  cnfval  20173  cnpfval  20174  cnpf2  20190  cnprcl2  20191  ssidcn  20195  iscnp4  20203  iscncl  20209  cncls2  20213  cncls  20214  cnntr  20215  cncnp  20220  lmcls  20242  lmcld  20243  iscnrm2  20278  ist0-2  20284  ist1-2  20287  ishaus2  20291  isreg2  20317  ordtt1  20319  sscmp  20344  dfcon2  20358  clscon  20369  concompcld  20373  1stccnp  20401  locfincf  20470  kgenval  20474  kgenuni  20478  1stckgenlem  20492  kgen2ss  20494  kgencn2  20496  txtopon  20530  txuni  20531  pttopon  20535  ptuniconst  20537  txcls  20543  ptclsg  20554  dfac14lem  20556  xkoccn  20558  ptcnplem  20560  ptcn  20566  cnmpt1t  20604  cnmpt2t  20612  cnmpt1res  20615  cnmpt2res  20616  cnmptkp  20619  cnmptk1p  20624  cnmptk2  20625  xkoinjcn  20626  elqtop3  20642  qtoptopon  20643  qtopcld  20652  qtoprest  20656  qtopcmap  20658  kqval  20665  kqcldsat  20672  isr0  20676  r0cld  20677  regr1lem  20678  kqnrmlem1  20682  kqnrmlem2  20683  pt1hmeo  20745  xpstopnlem1  20748  neifil  20819  trnei  20831  elflim  20910  flimss2  20911  flimss1  20912  flimopn  20914  fbflim2  20916  flimclslem  20923  flffval  20928  flfnei  20930  cnpflf2  20939  cnflf  20941  cnflf2  20942  isfcls2  20952  fclsopn  20953  fclsnei  20958  fclscmp  20969  ufilcmp  20971  fcfval  20972  fcfnei  20974  fcfelbas  20975  cnpfcf  20980  cnfcf  20981  alexsublem  20983  tmdcn2  21028  tmdgsum  21034  tmdgsum2  21035  symgtgp  21040  subgntr  21045  opnsubg  21046  clssubg  21047  clsnsg  21048  cldsubg  21049  tgpconcompeqg  21050  tgpconcomp  21051  ghmcnp  21053  snclseqg  21054  tgphaus  21055  tgpt1  21056  prdstmdd  21062  prdstgpd  21063  tsmsgsum  21077  tsmsid  21078  tsmsmhm  21084  tsmsadd  21085  tgptsmscld  21089  utop3cls  21190  mopnuni  21380  isxms2  21387  prdsxmslem2  21468  metdseq0  21795  cnmpt2pc  21865  ishtpy  21909  om1val  21967  pi1val  21974  csscld  22126  clsocv  22127  cfilfcls  22150  relcmpcmet  22192  limcres  22735  limccnp  22740  limccnp2  22741  dvbss  22750  perfdvf  22752  dvreslem  22758  dvres2lem  22759  dvcnp2  22768  dvaddbr  22786  dvmulbr  22787  dvcmulf  22793  dvmptres2  22810  dvmptcmul  22812  dvmptntr  22819  dvcnvrelem2  22864  ftc1cn  22889  taylthlem1  23219  ulmdvlem3  23248  efrlim  23786  pl1cn  28626  cvxpcon  29779  cvxscon  29780  ivthALT  30802  neibastop2  30828  neibastop3  30829  topmeet  30831  topjoin  30832  refsum2cnlem1  37031  dvresntr  37393
  Copyright terms: Public domain W3C validator