Theorem toponuni 20767

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

Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030  ∪ cuni 4468  ‘cfv 5926  Topctop 20746  TopOnctopon 20763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fv 5934  df-topon 20764

This theorem is referenced by:  toponunii  20769  toponmax  20778  toponss  20779  toponcom  20780  topgele  20782  topontopn  20792  toponmre  20945  cldmreon  20946  restuni  21014  resttopon2  21020  restlp  21035  restperf  21036  perfopn  21037  ordtcld1  21049  ordtcld2  21050  lmfval  21084  cnfval  21085  cnpfval  21086  cnpf2  21102  cnprcl2  21103  ssidcn  21107  iscnp4  21115  iscncl  21121  cncls2  21125  cncls  21126  cnntr  21127  cncnp  21132  lmcls  21154  lmcld  21155  iscnrm2  21190  ist0-2  21196  ist1-2  21199  ishaus2  21203  isreg2  21229  ordtt1  21231  sscmp  21256  dfconn2  21270  clsconn  21281  conncompcld  21285  1stccnp  21313  locfincf  21382  kgenval  21386  kgenuni  21390  1stckgenlem  21404  kgen2ss  21406  kgencn2  21408  txtopon  21442  txuni  21443  pttopon  21447  ptuniconst  21449  txcls  21455  ptclsg  21466  dfac14lem  21468  xkoccn  21470  ptcnplem  21472  ptcn  21478  cnmpt1t  21516  cnmpt2t  21524  cnmpt1res  21527  cnmpt2res  21528  cnmptkp  21531  cnmptk1p  21536  cnmptk2  21537  xkoinjcn  21538  elqtop3  21554  qtoptopon  21555  qtopcld  21564  qtoprest  21568  qtopcmap  21570  kqval  21577  kqcldsat  21584  isr0  21588  r0cld  21589  regr1lem  21590  kqnrmlem1  21594  kqnrmlem2  21595  pt1hmeo  21657  xpstopnlem1  21660  neifil  21731  trnei  21743  elflim  21822  flimss2  21823  flimss1  21824  flimopn  21826  fbflim2  21828  flimclslem  21835  flffval  21840  flfnei  21842  cnpflf2  21851  cnflf  21853  cnflf2  21854  isfcls2  21864  fclsopn  21865  fclsnei  21870  fclscmp  21881  ufilcmp  21883  fcfval  21884  fcfnei  21886  fcfelbas  21887  cnpfcf  21892  cnfcf  21893  alexsublem  21895  tmdcn2  21940  tmdgsum  21946  tmdgsum2  21947  symgtgp  21952  subgntr  21957  opnsubg  21958  clssubg  21959  clsnsg  21960  cldsubg  21961  tgpconncompeqg  21962  tgpconncomp  21963  ghmcnp  21965  snclseqg  21966  tgphaus  21967  tgpt1  21968  prdstmdd  21974  prdstgpd  21975  tsmsgsum  21989  tsmsid  21990  tsmsmhm  21996  tsmsadd  21997  tgptsmscld  22001  utop3cls  22102  mopnuni  22293  isxms2  22300  prdsxmslem2  22381  metdseq0  22704  cnmpt2pc  22774  ishtpy  22818  om1val  22876  pi1val  22883  csscld  23094  clsocv  23095  cfilfcls  23118  relcmpcmet  23161  limcres  23695  limccnp  23700  limccnp2  23701  dvbss  23710  perfdvf  23712  dvreslem  23718  dvres2lem  23719  dvcnp2  23728  dvaddbr  23746  dvmulbr  23747  dvcmulf  23753  dvmptres2  23770  dvmptcmul  23772  dvmptntr  23779  dvcnvrelem2  23826  ftc1cn  23851  taylthlem1  24172  ulmdvlem3  24201  efrlim  24741  pl1cn  30129  cvxpconn  31350  cvxsconn  31351  ivthALT  32455  neibastop2  32481  neibastop3  32482  topmeet  32484  topjoin  32485  refsum2cnlem1  39510  dvresntr  40450  rrxunitopnfi  40830