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

Theorem toponuni 18507
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 18505 . 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 1369    e. wcel 1756   U.cuni 4086   ` cfv 5413   Topctop 18473  TopOnctopon 18474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-iota 5376  df-fun 5415  df-fv 5421  df-topon 18481
This theorem is referenced by:  toponmax  18508  toponss  18509  toponcom  18510  toponunii  18512  topgele  18514  topontopn  18522  toponmre  18672  cldmreon  18673  restuni  18741  resttopon2  18747  restlp  18762  restperf  18763  perfopn  18764  ordtcld1  18776  ordtcld2  18777  lmfval  18811  cnfval  18812  cnpfval  18813  cnpf2  18829  cnprcl2  18830  ssidcn  18834  iscnp4  18842  iscncl  18848  cncls2  18852  cncls  18853  cnntr  18854  cncnp  18859  lmcls  18881  lmcld  18882  iscnrm2  18917  ist0-2  18923  ist1-2  18926  ishaus2  18930  isreg2  18956  ordtt1  18958  sscmp  18983  dfcon2  18998  clscon  19009  concompcld  19013  1stccnp  19041  kgenval  19083  kgenuni  19087  1stckgenlem  19101  kgen2ss  19103  kgencn2  19105  txtopon  19139  txuni  19140  pttopon  19144  ptuniconst  19146  txcls  19152  ptclsg  19163  dfac14lem  19165  xkoccn  19167  ptcnplem  19169  ptcn  19175  cnmpt1t  19213  cnmpt2t  19221  cnmpt1res  19224  cnmpt2res  19225  cnmptkp  19228  cnmptk1p  19233  cnmptk2  19234  xkoinjcn  19235  elqtop3  19251  qtoptopon  19252  qtopcld  19261  qtoprest  19265  qtopcmap  19267  kqval  19274  kqcldsat  19281  isr0  19285  r0cld  19286  regr1lem  19287  kqnrmlem1  19291  kqnrmlem2  19292  pt1hmeo  19354  xpstopnlem1  19357  neifil  19428  trnei  19440  elflim  19519  flimss2  19520  flimss1  19521  flimopn  19523  fbflim2  19525  flimclslem  19532  flffval  19537  flfnei  19539  cnpflf2  19548  cnflf  19550  cnflf2  19551  isfcls2  19561  fclsopn  19562  fclsnei  19567  fclscmp  19578  ufilcmp  19580  fcfval  19581  fcfnei  19583  fcfelbas  19584  cnpfcf  19589  cnfcf  19590  alexsublem  19591  tmdcn2  19635  tmdgsum  19641  tmdgsum2  19642  symgtgp  19647  subgntr  19652  opnsubg  19653  clssubg  19654  clsnsg  19655  cldsubg  19656  tgpconcompeqg  19657  tgpconcomp  19658  ghmcnp  19660  snclseqg  19661  tgphaus  19662  tgpt1  19663  prdstmdd  19669  prdstgpd  19670  tsmsgsum  19684  tsmsid  19685  tsmsgsumOLD  19687  tsmsidOLD  19688  tsmsmhm  19695  tsmsadd  19696  tgptsmscld  19700  utop3cls  19801  mopnuni  19991  isxms2  19998  prdsxmslem2  20079  metdseq0  20405  cnmpt2pc  20475  ishtpy  20519  om1val  20577  pi1val  20584  csscld  20736  clsocv  20737  cfilfcls  20760  relcmpcmet  20802  limcres  21336  limccnp  21341  limccnp2  21342  dvbss  21351  perfdvf  21353  dvreslem  21359  dvres2lem  21360  dvcnp2  21369  dvaddbr  21387  dvmulbr  21388  dvcmulf  21394  dvmptres2  21411  dvmptcmul  21413  dvmptntr  21420  dvcnvrelem2  21465  ftc1cn  21490  taylthlem1  21813  ulmdvlem3  21842  efrlim  22338  pl1cn  26337  cvxpcon  27083  cvxscon  27084  ivthALT  28483  locfincf  28531  neibastop2  28535  neibastop3  28536  topmeet  28538  topjoin  28539  refsum2cnlem1  29712
  Copyright terms: Public domain W3C validator