Theorem toponuni 22941

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ∪ cuni 4931  ‘cfv 6573  Topctop 22920  TopOnctopon 22937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581  df-topon 22938

This theorem is referenced by:  toponunii  22943  toponmax  22953  toponss  22954  toponcom  22955  topgele  22957  topontopn  22967  toponmre  23122  cldmreon  23123  restuni  23191  resttopon2  23197  restlp  23212  restperf  23213  perfopn  23214  ordtcld1  23226  ordtcld2  23227  lmfval  23261  cnfval  23262  cnpfval  23263  cnpf2  23279  cnprcl2  23280  ssidcn  23284  iscnp4  23292  iscncl  23298  cncls2  23302  cncls  23303  cnntr  23304  cncnp  23309  lmcls  23331  lmcld  23332  iscnrm2  23367  ist0-2  23373  ist1-2  23376  ishaus2  23380  isreg2  23406  ordtt1  23408  sscmp  23434  dfconn2  23448  clsconn  23459  conncompcld  23463  1stccnp  23491  locfincf  23560  kgenval  23564  kgenuni  23568  1stckgenlem  23582  kgen2ss  23584  kgencn2  23586  txtopon  23620  txuni  23621  pttopon  23625  ptuniconst  23627  txcls  23633  ptclsg  23644  dfac14lem  23646  xkoccn  23648  ptcnplem  23650  ptcn  23656  cnmpt1t  23694  cnmpt2t  23702  cnmpt1res  23705  cnmpt2res  23706  cnmptkp  23709  cnmptk1p  23714  cnmptk2  23715  xkoinjcn  23716  elqtop3  23732  qtoptopon  23733  qtopcld  23742  qtoprest  23746  qtopcmap  23748  kqval  23755  kqcldsat  23762  isr0  23766  r0cld  23767  regr1lem  23768  kqnrmlem1  23772  kqnrmlem2  23773  pt1hmeo  23835  xpstopnlem1  23838  neifil  23909  trnei  23921  elflim  24000  flimss2  24001  flimss1  24002  flimopn  24004  fbflim2  24006  flimclslem  24013  flffval  24018  flfnei  24020  cnpflf2  24029  cnflf  24031  cnflf2  24032  isfcls2  24042  fclsopn  24043  fclsnei  24048  fclscmp  24059  ufilcmp  24061  fcfval  24062  fcfnei  24064  fcfelbas  24065  cnpfcf  24070  cnfcf  24071  alexsublem  24073  tmdcn2  24118  tmdgsum  24124  tmdgsum2  24125  symgtgp  24135  subgntr  24136  opnsubg  24137  clssubg  24138  clsnsg  24139  cldsubg  24140  tgpconncompeqg  24141  tgpconncomp  24142  ghmcnp  24144  snclseqg  24145  tgphaus  24146  tgpt1  24147  prdstmdd  24153  prdstgpd  24154  tsmsgsum  24168  tsmsid  24169  tsmsmhm  24175  tsmsadd  24176  tgptsmscld  24180  utop3cls  24281  mopnuni  24472  isxms2  24479  prdsxmslem2  24563  metdseq0  24895  cnmpopc  24974  ishtpy  25023  om1val  25082  pi1val  25089  csscld  25302  clsocv  25303  cfilfcls  25327  relcmpcmet  25371  limcres  25941  limccnp  25946  limccnp2  25947  dvbss  25956  perfdvf  25958  dvreslem  25964  dvres2lem  25965  dvcnp2  25975  dvcnp2OLD  25976  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcmulf  26002  dvmptres2  26020  dvmptcmul  26022  dvmptntr  26029  dvcnvrelem2  26077  ftc1cn  26104  taylthlem1  26433  ulmdvlem3  26463  efrlim  27030  efrlimOLD  27031  zart0  33825  zarmxt1  33826  pl1cn  33901  cvxpconn  35210  cvxsconn  35211  ivthALT  36301  neibastop2  36327  neibastop3  36328  topmeet  36330  topjoin  36331  refsum2cnlem1  44937  dvresntr  45839  rrxunitopnfi  46213