Theorem toponuni 23039

Description: The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)

Assertion

Ref	Expression
toponuni	⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)

Proof of Theorem toponuni

Step	Hyp	Ref	Expression
1		istopon 23037	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
2	1	simprbi 502	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ∪ cuni 4876  ‘cfv 6537  Topctop 23018  TopOnctopon 23035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-iota 6493  df-fun 6539  df-fv 6545  df-topon 23036

This theorem is referenced by:  toponunii  23041  toponmax  23051  toponss  23052  toponcom  23053  topgele  23055  topontopn  23065  toponmre  23218  cldmreon  23219  restuni  23287  resttopon2  23293  restlp  23308  restperf  23309  perfopn  23310  ordtcld1  23322  ordtcld2  23323  lmfval  23357  cnfval  23358  cnpfval  23359  cnpf2  23375  cnprcl2  23376  ssidcn  23380  iscnp4  23388  iscncl  23394  cncls2  23398  cncls  23399  cnntr  23400  cncnp  23405  lmcls  23427  lmcld  23428  iscnrm2  23463  ist0-2  23469  ist1-2  23472  ishaus2  23476  isreg2  23502  ordtt1  23504  sscmp  23530  dfconn2  23544  clsconn  23555  conncompcld  23559  1stccnp  23587  locfincf  23656  kgenval  23660  kgenuni  23664  1stckgenlem  23678  kgen2ss  23680  kgencn2  23682  txtopon  23716  txuni  23717  pttopon  23721  ptuniconst  23723  txcls  23729  ptclsg  23740  dfac14lem  23742  xkoccn  23744  ptcnplem  23746  ptcn  23752  cnmpt1t  23790  cnmpt2t  23798  cnmpt1res  23801  cnmpt2res  23802  cnmptkp  23805  cnmptk1p  23810  cnmptk2  23811  xkoinjcn  23812  elqtop3  23828  qtoptopon  23829  qtopcld  23838  qtoprest  23842  qtopcmap  23844  kqval  23851  kqcldsat  23858  isr0  23862  r0cld  23863  regr1lem  23864  kqnrmlem1  23868  kqnrmlem2  23869  pt1hmeo  23931  xpstopnlem1  23934  neifil  24005  trnei  24017  elflim  24096  flimss2  24097  flimss1  24098  flimopn  24100  fbflim2  24102  flimclslem  24109  flffval  24114  flfnei  24116  cnpflf2  24125  cnflf  24127  cnflf2  24128  isfcls2  24138  fclsopn  24139  fclsnei  24144  fclscmp  24155  ufilcmp  24157  fcfval  24158  fcfnei  24160  fcfelbas  24161  cnpfcf  24166  cnfcf  24167  alexsublem  24169  tmdcn2  24214  tmdgsum  24220  tmdgsum2  24221  symgtgp  24231  subgntr  24232  opnsubg  24233  clssubg  24234  clsnsg  24235  cldsubg  24236  tgpconncompeqg  24237  tgpconncomp  24238  ghmcnp  24240  snclseqg  24241  tgphaus  24242  tgpt1  24243  prdstmdd  24249  prdstgpd  24250  tsmsgsum  24264  tsmsid  24265  tsmsmhm  24271  tsmsadd  24272  tgptsmscld  24276  utop3cls  24376  mopnuni  24566  isxms2  24573  prdsxmslem2  24654  metdseq0  24980  cnmpopc  25055  ishtpy  25099  om1val  25157  pi1val  25164  csscld  25376  clsocv  25377  cfilfcls  25401  relcmpcmet  25445  limcres  26013  limccnp  26018  limccnp2  26019  dvbss  26028  perfdvf  26030  dvreslem  26036  dvres2lem  26037  dvcnp2  26047  dvaddbr  26065  dvmulbr  26066  dvcmulf  26072  dvmptres2  26089  dvmptcmul  26091  dvmptntr  26098  dvcnvrelem2  26145  ftc1cn  26170  taylthlem1  26501  ulmdvlem3  26530  efrlim  27099  zart0  34213  zarmxt1  34214  pl1cn  34289  cvxpconn  35632  cvxsconn  35633  ivthALT  36734  neibastop2  36760  neibastop3  36761  topmeet  36763  topjoin  36764  refsum2cnlem1  45648  dvresntr  46523  rrxunitopnfi  46897