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

Theorem toponuni 19935
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 19933 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simprbi 466 1  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1443    e. wcel 1886   U.cuni 4197   ` cfv 5581   Topctop 19910  TopOnctopon 19911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-iota 5545  df-fun 5583  df-fv 5589  df-topon 19916
This theorem is referenced by:  toponmax  19936  toponss  19937  toponcom  19938  toponunii  19940  topgele  19942  topontopn  19950  toponmre  20102  cldmreon  20103  restuni  20171  resttopon2  20177  restlp  20192  restperf  20193  perfopn  20194  ordtcld1  20206  ordtcld2  20207  lmfval  20241  cnfval  20242  cnpfval  20243  cnpf2  20259  cnprcl2  20260  ssidcn  20264  iscnp4  20272  iscncl  20278  cncls2  20282  cncls  20283  cnntr  20284  cncnp  20289  lmcls  20311  lmcld  20312  iscnrm2  20347  ist0-2  20353  ist1-2  20356  ishaus2  20360  isreg2  20386  ordtt1  20388  sscmp  20413  dfcon2  20427  clscon  20438  concompcld  20442  1stccnp  20470  locfincf  20539  kgenval  20543  kgenuni  20547  1stckgenlem  20561  kgen2ss  20563  kgencn2  20565  txtopon  20599  txuni  20600  pttopon  20604  ptuniconst  20606  txcls  20612  ptclsg  20623  dfac14lem  20625  xkoccn  20627  ptcnplem  20629  ptcn  20635  cnmpt1t  20673  cnmpt2t  20681  cnmpt1res  20684  cnmpt2res  20685  cnmptkp  20688  cnmptk1p  20693  cnmptk2  20694  xkoinjcn  20695  elqtop3  20711  qtoptopon  20712  qtopcld  20721  qtoprest  20725  qtopcmap  20727  kqval  20734  kqcldsat  20741  isr0  20745  r0cld  20746  regr1lem  20747  kqnrmlem1  20751  kqnrmlem2  20752  pt1hmeo  20814  xpstopnlem1  20817  neifil  20888  trnei  20900  elflim  20979  flimss2  20980  flimss1  20981  flimopn  20983  fbflim2  20985  flimclslem  20992  flffval  20997  flfnei  20999  cnpflf2  21008  cnflf  21010  cnflf2  21011  isfcls2  21021  fclsopn  21022  fclsnei  21027  fclscmp  21038  ufilcmp  21040  fcfval  21041  fcfnei  21043  fcfelbas  21044  cnpfcf  21049  cnfcf  21050  alexsublem  21052  tmdcn2  21097  tmdgsum  21103  tmdgsum2  21104  symgtgp  21109  subgntr  21114  opnsubg  21115  clssubg  21116  clsnsg  21117  cldsubg  21118  tgpconcompeqg  21119  tgpconcomp  21120  ghmcnp  21122  snclseqg  21123  tgphaus  21124  tgpt1  21125  prdstmdd  21131  prdstgpd  21132  tsmsgsum  21146  tsmsid  21147  tsmsmhm  21153  tsmsadd  21154  tgptsmscld  21158  utop3cls  21259  mopnuni  21449  isxms2  21456  prdsxmslem2  21537  metdseq0  21864  metdseq0OLD  21879  cnmpt2pc  21949  ishtpy  21996  om1val  22054  pi1val  22061  csscld  22213  clsocv  22214  cfilfcls  22237  relcmpcmet  22279  limcres  22834  limccnp  22839  limccnp2  22840  dvbss  22849  perfdvf  22851  dvreslem  22857  dvres2lem  22858  dvcnp2  22867  dvaddbr  22885  dvmulbr  22886  dvcmulf  22892  dvmptres2  22909  dvmptcmul  22911  dvmptntr  22918  dvcnvrelem2  22963  ftc1cn  22988  taylthlem1  23321  ulmdvlem3  23350  efrlim  23888  pl1cn  28754  cvxpcon  29958  cvxscon  29959  ivthALT  30984  neibastop2  31010  neibastop3  31011  topmeet  31013  topjoin  31014  refsum2cnlem1  37352  dvresntr  37782  rrxunitopnfi  38155
  Copyright terms: Public domain W3C validator