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

Theorem toponuni 18667
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 18665 . 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 1370    e. wcel 1758   U.cuni 4202   ` cfv 5529   Topctop 18633  TopOnctopon 18634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-iota 5492  df-fun 5531  df-fv 5537  df-topon 18641
This theorem is referenced by:  toponmax  18668  toponss  18669  toponcom  18670  toponunii  18672  topgele  18674  topontopn  18682  toponmre  18832  cldmreon  18833  restuni  18901  resttopon2  18907  restlp  18922  restperf  18923  perfopn  18924  ordtcld1  18936  ordtcld2  18937  lmfval  18971  cnfval  18972  cnpfval  18973  cnpf2  18989  cnprcl2  18990  ssidcn  18994  iscnp4  19002  iscncl  19008  cncls2  19012  cncls  19013  cnntr  19014  cncnp  19019  lmcls  19041  lmcld  19042  iscnrm2  19077  ist0-2  19083  ist1-2  19086  ishaus2  19090  isreg2  19116  ordtt1  19118  sscmp  19143  dfcon2  19158  clscon  19169  concompcld  19173  1stccnp  19201  kgenval  19243  kgenuni  19247  1stckgenlem  19261  kgen2ss  19263  kgencn2  19265  txtopon  19299  txuni  19300  pttopon  19304  ptuniconst  19306  txcls  19312  ptclsg  19323  dfac14lem  19325  xkoccn  19327  ptcnplem  19329  ptcn  19335  cnmpt1t  19373  cnmpt2t  19381  cnmpt1res  19384  cnmpt2res  19385  cnmptkp  19388  cnmptk1p  19393  cnmptk2  19394  xkoinjcn  19395  elqtop3  19411  qtoptopon  19412  qtopcld  19421  qtoprest  19425  qtopcmap  19427  kqval  19434  kqcldsat  19441  isr0  19445  r0cld  19446  regr1lem  19447  kqnrmlem1  19451  kqnrmlem2  19452  pt1hmeo  19514  xpstopnlem1  19517  neifil  19588  trnei  19600  elflim  19679  flimss2  19680  flimss1  19681  flimopn  19683  fbflim2  19685  flimclslem  19692  flffval  19697  flfnei  19699  cnpflf2  19708  cnflf  19710  cnflf2  19711  isfcls2  19721  fclsopn  19722  fclsnei  19727  fclscmp  19738  ufilcmp  19740  fcfval  19741  fcfnei  19743  fcfelbas  19744  cnpfcf  19749  cnfcf  19750  alexsublem  19751  tmdcn2  19795  tmdgsum  19801  tmdgsum2  19802  symgtgp  19807  subgntr  19812  opnsubg  19813  clssubg  19814  clsnsg  19815  cldsubg  19816  tgpconcompeqg  19817  tgpconcomp  19818  ghmcnp  19820  snclseqg  19821  tgphaus  19822  tgpt1  19823  prdstmdd  19829  prdstgpd  19830  tsmsgsum  19844  tsmsid  19845  tsmsgsumOLD  19847  tsmsidOLD  19848  tsmsmhm  19855  tsmsadd  19856  tgptsmscld  19860  utop3cls  19961  mopnuni  20151  isxms2  20158  prdsxmslem2  20239  metdseq0  20565  cnmpt2pc  20635  ishtpy  20679  om1val  20737  pi1val  20744  csscld  20896  clsocv  20897  cfilfcls  20920  relcmpcmet  20962  limcres  21497  limccnp  21502  limccnp2  21503  dvbss  21512  perfdvf  21514  dvreslem  21520  dvres2lem  21521  dvcnp2  21530  dvaddbr  21548  dvmulbr  21549  dvcmulf  21555  dvmptres2  21572  dvmptcmul  21574  dvmptntr  21581  dvcnvrelem2  21626  ftc1cn  21651  taylthlem1  21974  ulmdvlem3  22003  efrlim  22499  pl1cn  26550  cvxpcon  27295  cvxscon  27296  ivthALT  28698  locfincf  28746  neibastop2  28750  neibastop3  28751  topmeet  28753  topjoin  28754  refsum2cnlem1  29927
  Copyright terms: Public domain W3C validator