Theorem toponuni 22636

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 22634	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
2	1	simprbi 495	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  ∪ cuni 4907  ‘cfv 6542  Topctop 22615  TopOnctopon 22632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6494  df-fun 6544  df-fv 6550  df-topon 22633

This theorem is referenced by:  toponunii  22638  toponmax  22648  toponss  22649  toponcom  22650  topgele  22652  topontopn  22662  toponmre  22817  cldmreon  22818  restuni  22886  resttopon2  22892  restlp  22907  restperf  22908  perfopn  22909  ordtcld1  22921  ordtcld2  22922  lmfval  22956  cnfval  22957  cnpfval  22958  cnpf2  22974  cnprcl2  22975  ssidcn  22979  iscnp4  22987  iscncl  22993  cncls2  22997  cncls  22998  cnntr  22999  cncnp  23004  lmcls  23026  lmcld  23027  iscnrm2  23062  ist0-2  23068  ist1-2  23071  ishaus2  23075  isreg2  23101  ordtt1  23103  sscmp  23129  dfconn2  23143  clsconn  23154  conncompcld  23158  1stccnp  23186  locfincf  23255  kgenval  23259  kgenuni  23263  1stckgenlem  23277  kgen2ss  23279  kgencn2  23281  txtopon  23315  txuni  23316  pttopon  23320  ptuniconst  23322  txcls  23328  ptclsg  23339  dfac14lem  23341  xkoccn  23343  ptcnplem  23345  ptcn  23351  cnmpt1t  23389  cnmpt2t  23397  cnmpt1res  23400  cnmpt2res  23401  cnmptkp  23404  cnmptk1p  23409  cnmptk2  23410  xkoinjcn  23411  elqtop3  23427  qtoptopon  23428  qtopcld  23437  qtoprest  23441  qtopcmap  23443  kqval  23450  kqcldsat  23457  isr0  23461  r0cld  23462  regr1lem  23463  kqnrmlem1  23467  kqnrmlem2  23468  pt1hmeo  23530  xpstopnlem1  23533  neifil  23604  trnei  23616  elflim  23695  flimss2  23696  flimss1  23697  flimopn  23699  fbflim2  23701  flimclslem  23708  flffval  23713  flfnei  23715  cnpflf2  23724  cnflf  23726  cnflf2  23727  isfcls2  23737  fclsopn  23738  fclsnei  23743  fclscmp  23754  ufilcmp  23756  fcfval  23757  fcfnei  23759  fcfelbas  23760  cnpfcf  23765  cnfcf  23766  alexsublem  23768  tmdcn2  23813  tmdgsum  23819  tmdgsum2  23820  symgtgp  23830  subgntr  23831  opnsubg  23832  clssubg  23833  clsnsg  23834  cldsubg  23835  tgpconncompeqg  23836  tgpconncomp  23837  ghmcnp  23839  snclseqg  23840  tgphaus  23841  tgpt1  23842  prdstmdd  23848  prdstgpd  23849  tsmsgsum  23863  tsmsid  23864  tsmsmhm  23870  tsmsadd  23871  tgptsmscld  23875  utop3cls  23976  mopnuni  24167  isxms2  24174  prdsxmslem2  24258  metdseq0  24590  cnmpopc  24669  ishtpy  24718  om1val  24777  pi1val  24784  csscld  24997  clsocv  24998  cfilfcls  25022  relcmpcmet  25066  limcres  25635  limccnp  25640  limccnp2  25641  dvbss  25650  perfdvf  25652  dvreslem  25658  dvres2lem  25659  dvcnp2  25669  dvcnp2OLD  25670  dvaddbr  25688  dvmulbr  25689  dvmulbrOLD  25690  dvcmulf  25696  dvmptres2  25714  dvmptcmul  25716  dvmptntr  25723  dvcnvrelem2  25770  ftc1cn  25795  taylthlem1  26121  ulmdvlem3  26150  efrlim  26710  zart0  33157  zarmxt1  33158  pl1cn  33233  cvxpconn  34531  cvxsconn  34532  ivthALT  35523  neibastop2  35549  neibastop3  35550  topmeet  35552  topjoin  35553  refsum2cnlem1  44023  dvresntr  44932  rrxunitopnfi  45306