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

Theorem toponuni 16984
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 16982 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simprbi 451 1  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725   U.cuni 4007   ` cfv 5446   Topctop 16950  TopOnctopon 16951
This theorem is referenced by:  toponmax  16985  toponss  16986  toponcom  16987  toponunii  16989  topgele  16991  topontopn  16999  toponmre  17149  cldmreon  17150  restuni  17218  resttopon2  17224  restlp  17239  restperf  17240  perfopn  17241  ordtcld1  17253  ordtcld2  17254  lmfval  17288  cnfval  17289  cnpfval  17290  cnpf2  17306  cnprcl2  17307  ssidcn  17311  iscnp4  17319  iscncl  17325  cncls2  17329  cncls  17330  cnntr  17331  cncnp  17336  lmcls  17358  lmcld  17359  iscnrm2  17394  ist0-2  17400  ist1-2  17403  ishaus2  17407  isreg2  17433  ordtt1  17435  sscmp  17460  dfcon2  17474  clscon  17485  concompcld  17489  1stccnp  17517  kgenval  17559  kgenuni  17563  1stckgenlem  17577  kgen2ss  17579  kgencn2  17581  txtopon  17615  txuni  17616  pttopon  17620  ptuniconst  17622  txcls  17628  ptclsg  17639  dfac14lem  17641  xkoccn  17643  ptcnplem  17645  ptcn  17651  cnmpt1t  17689  cnmpt2t  17697  cnmpt1res  17700  cnmpt2res  17701  cnmptkp  17704  cnmptk1p  17709  cnmptk2  17710  xkoinjcn  17711  elqtop3  17727  qtoptopon  17728  qtopcld  17737  qtoprest  17741  qtopcmap  17743  kqval  17750  kqcldsat  17757  isr0  17761  r0cld  17762  regr1lem  17763  kqnrmlem1  17767  kqnrmlem2  17768  pt1hmeo  17830  xpstopnlem1  17833  neifil  17904  trnei  17916  elflim  17995  flimss2  17996  flimss1  17997  flimopn  17999  fbflim2  18001  flimclslem  18008  flffval  18013  flfnei  18015  cnpflf2  18024  cnflf  18026  cnflf2  18027  isfcls2  18037  fclsopn  18038  fclsnei  18043  fclscmp  18054  ufilcmp  18056  fcfval  18057  fcfnei  18059  fcfelbas  18060  cnpfcf  18065  cnfcf  18066  alexsublem  18067  tmdcn2  18111  tmdgsum  18117  tmdgsum2  18118  symgtgp  18123  subgntr  18128  opnsubg  18129  clssubg  18130  clsnsg  18131  cldsubg  18132  tgpconcompeqg  18133  tgpconcomp  18134  ghmcnp  18136  snclseqg  18137  tgphaus  18138  tgpt1  18139  prdstmdd  18145  prdstgpd  18146  tsmsgsum  18160  tsmsid  18161  tsmsmhm  18167  tsmsadd  18168  tgptsmscld  18172  utop3cls  18273  mopnuni  18463  isxms2  18470  prdsxmslem2  18551  metdseq0  18876  cnmpt2pc  18945  ishtpy  18989  om1val  19047  pi1val  19054  csscld  19195  clsocv  19196  cfilfcls  19219  relcmpcmet  19261  limcres  19765  limccnp  19770  limccnp2  19771  dvbss  19780  perfdvf  19782  dvreslem  19788  dvres2lem  19789  dvcnp2  19798  dvaddbr  19816  dvmulbr  19817  dvcmulf  19823  dvmptres2  19840  dvmptcmul  19842  dvmptntr  19849  dvcnvrelem2  19894  ftc1cn  19919  taylthlem1  20281  ulmdvlem3  20310  efrlim  20800  cvxpcon  24921  cvxscon  24922  ivthALT  26329  locfincf  26377  neibastop2  26381  neibastop3  26382  topmeet  26384  topjoin  26385  refsum2cnlem1  27675
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-iota 5410  df-fun 5448  df-fv 5454  df-topon 16958
  Copyright terms: Public domain W3C validator