Theorem toponuni 20719

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

Step	Hyp	Ref	Expression
1		istopon 20717	. 2 |- ( J e. (TopOn ` B ) <-> ( J e. Top /\ B = U. J ) )
2	1	simprbi 480	1 |- ( J e. (TopOn ` B ) -> B = U. J )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   U.cuni 4436   ` cfv 5888   Topctop 20698  TopOnctopon 20715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-topon 20716

This theorem is referenced by:  toponunii  20721  toponmax  20730  toponss  20731  toponcom  20732  topgele  20734  topontopn  20744  toponmre  20897  cldmreon  20898  restuni  20966  resttopon2  20972  restlp  20987  restperf  20988  perfopn  20989  ordtcld1  21001  ordtcld2  21002  lmfval  21036  cnfval  21037  cnpfval  21038  cnpf2  21054  cnprcl2  21055  ssidcn  21059  iscnp4  21067  iscncl  21073  cncls2  21077  cncls  21078  cnntr  21079  cncnp  21084  lmcls  21106  lmcld  21107  iscnrm2  21142  ist0-2  21148  ist1-2  21151  ishaus2  21155  isreg2  21181  ordtt1  21183  sscmp  21208  dfconn2  21222  clsconn  21233  conncompcld  21237  1stccnp  21265  locfincf  21334  kgenval  21338  kgenuni  21342  1stckgenlem  21356  kgen2ss  21358  kgencn2  21360  txtopon  21394  txuni  21395  pttopon  21399  ptuniconst  21401  txcls  21407  ptclsg  21418  dfac14lem  21420  xkoccn  21422  ptcnplem  21424  ptcn  21430  cnmpt1t  21468  cnmpt2t  21476  cnmpt1res  21479  cnmpt2res  21480  cnmptkp  21483  cnmptk1p  21488  cnmptk2  21489  xkoinjcn  21490  elqtop3  21506  qtoptopon  21507  qtopcld  21516  qtoprest  21520  qtopcmap  21522  kqval  21529  kqcldsat  21536  isr0  21540  r0cld  21541  regr1lem  21542  kqnrmlem1  21546  kqnrmlem2  21547  pt1hmeo  21609  xpstopnlem1  21612  neifil  21684  trnei  21696  elflim  21775  flimss2  21776  flimss1  21777  flimopn  21779  fbflim2  21781  flimclslem  21788  flffval  21793  flfnei  21795  cnpflf2  21804  cnflf  21806  cnflf2  21807  isfcls2  21817  fclsopn  21818  fclsnei  21823  fclscmp  21834  ufilcmp  21836  fcfval  21837  fcfnei  21839  fcfelbas  21840  cnpfcf  21845  cnfcf  21846  alexsublem  21848  tmdcn2  21893  tmdgsum  21899  tmdgsum2  21900  symgtgp  21905  subgntr  21910  opnsubg  21911  clssubg  21912  clsnsg  21913  cldsubg  21914  tgpconncompeqg  21915  tgpconncomp  21916  ghmcnp  21918  snclseqg  21919  tgphaus  21920  tgpt1  21921  prdstmdd  21927  prdstgpd  21928  tsmsgsum  21942  tsmsid  21943  tsmsmhm  21949  tsmsadd  21950  tgptsmscld  21954  utop3cls  22055  mopnuni  22246  isxms2  22253  prdsxmslem2  22334  metdseq0  22657  cnmpt2pc  22727  ishtpy  22771  om1val  22830  pi1val  22837  csscld  23048  clsocv  23049  cfilfcls  23072  relcmpcmet  23115  limcres  23650  limccnp  23655  limccnp2  23656  dvbss  23665  perfdvf  23667  dvreslem  23673  dvres2lem  23674  dvcnp2  23683  dvaddbr  23701  dvmulbr  23702  dvcmulf  23708  dvmptres2  23725  dvmptcmul  23727  dvmptntr  23734  dvcnvrelem2  23781  ftc1cn  23806  taylthlem1  24127  ulmdvlem3  24156  efrlim  24696  pl1cn  30001  cvxpconn  31224  cvxsconn  31225  ivthALT  32330  neibastop2  32356  neibastop3  32357  topmeet  32359  topjoin  32360  refsum2cnlem1  39196  dvresntr  40132  rrxunitopnfi  40512