Theorem toponuni 22783

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ cuni 4856  ‘cfv 6476  Topctop 22762  TopOnctopon 22779

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5367  ax-un 7662

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3393  df-v 3435  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-opab 5151  df-mpt 5170  df-id 5508  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-iota 6432  df-fun 6478  df-fv 6484  df-topon 22780

This theorem is referenced by:  toponunii  22785  toponmax  22795  toponss  22796  toponcom  22797  topgele  22799  topontopn  22809  toponmre  22962  cldmreon  22963  restuni  23031  resttopon2  23037  restlp  23052  restperf  23053  perfopn  23054  ordtcld1  23066  ordtcld2  23067  lmfval  23101  cnfval  23102  cnpfval  23103  cnpf2  23119  cnprcl2  23120  ssidcn  23124  iscnp4  23132  iscncl  23138  cncls2  23142  cncls  23143  cnntr  23144  cncnp  23149  lmcls  23171  lmcld  23172  iscnrm2  23207  ist0-2  23213  ist1-2  23216  ishaus2  23220  isreg2  23246  ordtt1  23248  sscmp  23274  dfconn2  23288  clsconn  23299  conncompcld  23303  1stccnp  23331  locfincf  23400  kgenval  23404  kgenuni  23408  1stckgenlem  23422  kgen2ss  23424  kgencn2  23426  txtopon  23460  txuni  23461  pttopon  23465  ptuniconst  23467  txcls  23473  ptclsg  23484  dfac14lem  23486  xkoccn  23488  ptcnplem  23490  ptcn  23496  cnmpt1t  23534  cnmpt2t  23542  cnmpt1res  23545  cnmpt2res  23546  cnmptkp  23549  cnmptk1p  23554  cnmptk2  23555  xkoinjcn  23556  elqtop3  23572  qtoptopon  23573  qtopcld  23582  qtoprest  23586  qtopcmap  23588  kqval  23595  kqcldsat  23602  isr0  23606  r0cld  23607  regr1lem  23608  kqnrmlem1  23612  kqnrmlem2  23613  pt1hmeo  23675  xpstopnlem1  23678  neifil  23749  trnei  23761  elflim  23840  flimss2  23841  flimss1  23842  flimopn  23844  fbflim2  23846  flimclslem  23853  flffval  23858  flfnei  23860  cnpflf2  23869  cnflf  23871  cnflf2  23872  isfcls2  23882  fclsopn  23883  fclsnei  23888  fclscmp  23899  ufilcmp  23901  fcfval  23902  fcfnei  23904  fcfelbas  23905  cnpfcf  23910  cnfcf  23911  alexsublem  23913  tmdcn2  23958  tmdgsum  23964  tmdgsum2  23965  symgtgp  23975  subgntr  23976  opnsubg  23977  clssubg  23978  clsnsg  23979  cldsubg  23980  tgpconncompeqg  23981  tgpconncomp  23982  ghmcnp  23984  snclseqg  23985  tgphaus  23986  tgpt1  23987  prdstmdd  23993  prdstgpd  23994  tsmsgsum  24008  tsmsid  24009  tsmsmhm  24015  tsmsadd  24016  tgptsmscld  24020  utop3cls  24120  mopnuni  24310  isxms2  24317  prdsxmslem2  24398  metdseq0  24724  cnmpopc  24803  ishtpy  24852  om1val  24911  pi1val  24918  csscld  25130  clsocv  25131  cfilfcls  25155  relcmpcmet  25199  limcres  25768  limccnp  25773  limccnp2  25774  dvbss  25783  perfdvf  25785  dvreslem  25791  dvres2lem  25792  dvcnp2  25802  dvcnp2OLD  25803  dvaddbr  25821  dvmulbr  25822  dvmulbrOLD  25823  dvcmulf  25829  dvmptres2  25847  dvmptcmul  25849  dvmptntr  25856  dvcnvrelem2  25904  ftc1cn  25931  taylthlem1  26262  ulmdvlem3  26292  efrlim  26860  efrlimOLD  26861  zart0  33860  zarmxt1  33861  pl1cn  33936  cvxpconn  35232  cvxsconn  35233  ivthALT  36326  neibastop2  36352  neibastop3  36353  topmeet  36355  topjoin  36356  refsum2cnlem1  45031  dvresntr  45913  rrxunitopnfi  46287