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

Theorem toponuni 16665
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 16663 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simprbi 450 1  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   U.cuni 3827   ` cfv 5255   Topctop 16631  TopOnctopon 16632
This theorem is referenced by:  toponmax  16666  toponss  16667  toponcom  16668  toponunii  16670  topgele  16672  topontopn  16680  toponmre  16830  cldmreon  16831  restuni  16893  resttopon2  16899  restlp  16913  restperf  16914  perfopn  16915  ordtcld1  16927  ordtcld2  16928  lmfval  16962  cnfval  16963  cnpfval  16964  cnpf2  16980  cnprcl2  16981  ssidcn  16985  iscncl  16998  cncls2  17002  cncls  17003  cnntr  17004  cncnp  17009  lmcls  17030  lmcld  17031  iscnrm2  17066  ist0-2  17072  ist1-2  17075  ishaus2  17079  isreg2  17105  ordtt1  17107  sscmp  17132  dfcon2  17145  clscon  17156  concompcld  17160  1stccnp  17188  kgenval  17230  kgenuni  17234  1stckgenlem  17248  kgen2ss  17250  kgencn2  17252  txtopon  17286  txuni  17287  pttopon  17291  ptuniconst  17293  txcls  17299  ptclsg  17309  dfac14lem  17311  xkoccn  17313  ptcnplem  17315  ptcn  17321  cnmpt1t  17359  cnmpt2t  17367  cnmpt1res  17370  cnmpt2res  17371  cnmptkp  17374  cnmptk1p  17379  cnmptk2  17380  xkoinjcn  17381  elqtop3  17394  qtoptopon  17395  qtopcld  17404  qtoprest  17408  qtopcmap  17410  kqval  17417  kqcldsat  17424  isr0  17428  r0cld  17429  regr1lem  17430  kqnrmlem1  17434  kqnrmlem2  17435  pt1hmeo  17497  xpstopnlem1  17500  neifil  17575  trnei  17587  elflim  17666  flimss2  17667  flimss1  17668  flimopn  17670  fbflim2  17672  flimclslem  17679  flffval  17684  flfnei  17686  cnpflf2  17695  cnflf  17697  cnflf2  17698  isfcls2  17708  fclsopn  17709  fclsnei  17714  fclscmp  17725  ufilcmp  17727  fcfval  17728  fcfnei  17730  fcfelbas  17731  cnpfcf  17736  cnfcf  17737  alexsublem  17738  tmdcn2  17772  tmdgsum  17778  tmdgsum2  17779  symgtgp  17784  subgntr  17789  opnsubg  17790  clssubg  17791  clsnsg  17792  cldsubg  17793  tgpconcompeqg  17794  tgpconcomp  17795  ghmcnp  17797  snclseqg  17798  tgphaus  17799  tgpt1  17800  prdstmdd  17806  prdstgpd  17807  tsmsgsum  17821  tsmsid  17822  tsmsmhm  17828  tsmsadd  17829  tgptsmscld  17833  mopnuni  17987  isxms2  17994  prdsxmslem2  18075  metdseq0  18358  cnmpt2pc  18426  ishtpy  18470  om1val  18528  pi1val  18535  csscld  18676  clsocv  18677  cfilfcls  18700  relcmpcmet  18742  limcres  19236  limccnp  19241  limccnp2  19242  dvbss  19251  perfdvf  19253  dvreslem  19259  dvres2lem  19260  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvcmulf  19294  dvmptres2  19311  dvmptcmul  19313  dvmptntr  19320  dvcnvrelem2  19365  ftc1cn  19390  taylthlem1  19752  ulmdvlem3  19779  efrlim  20264  tpr2uni  23288  tpr2rico  23296  cvxpcon  23773  cvxscon  23774  iscnp4  25563  ivthALT  26258  locfincf  26306  neibastop2  26310  neibastop3  26311  topmeet  26313  topjoin  26314  refsum2cnlem1  27708
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fv 5263  df-topon 16639
  Copyright terms: Public domain W3C validator