Theorem toponuni 22063

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  ∪ cuni 4839  ‘cfv 6433  Topctop 22042  TopOnctopon 22059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-topon 22060

This theorem is referenced by:  toponunii  22065  toponmax  22075  toponss  22076  toponcom  22077  topgele  22079  topontopn  22089  toponmre  22244  cldmreon  22245  restuni  22313  resttopon2  22319  restlp  22334  restperf  22335  perfopn  22336  ordtcld1  22348  ordtcld2  22349  lmfval  22383  cnfval  22384  cnpfval  22385  cnpf2  22401  cnprcl2  22402  ssidcn  22406  iscnp4  22414  iscncl  22420  cncls2  22424  cncls  22425  cnntr  22426  cncnp  22431  lmcls  22453  lmcld  22454  iscnrm2  22489  ist0-2  22495  ist1-2  22498  ishaus2  22502  isreg2  22528  ordtt1  22530  sscmp  22556  dfconn2  22570  clsconn  22581  conncompcld  22585  1stccnp  22613  locfincf  22682  kgenval  22686  kgenuni  22690  1stckgenlem  22704  kgen2ss  22706  kgencn2  22708  txtopon  22742  txuni  22743  pttopon  22747  ptuniconst  22749  txcls  22755  ptclsg  22766  dfac14lem  22768  xkoccn  22770  ptcnplem  22772  ptcn  22778  cnmpt1t  22816  cnmpt2t  22824  cnmpt1res  22827  cnmpt2res  22828  cnmptkp  22831  cnmptk1p  22836  cnmptk2  22837  xkoinjcn  22838  elqtop3  22854  qtoptopon  22855  qtopcld  22864  qtoprest  22868  qtopcmap  22870  kqval  22877  kqcldsat  22884  isr0  22888  r0cld  22889  regr1lem  22890  kqnrmlem1  22894  kqnrmlem2  22895  pt1hmeo  22957  xpstopnlem1  22960  neifil  23031  trnei  23043  elflim  23122  flimss2  23123  flimss1  23124  flimopn  23126  fbflim2  23128  flimclslem  23135  flffval  23140  flfnei  23142  cnpflf2  23151  cnflf  23153  cnflf2  23154  isfcls2  23164  fclsopn  23165  fclsnei  23170  fclscmp  23181  ufilcmp  23183  fcfval  23184  fcfnei  23186  fcfelbas  23187  cnpfcf  23192  cnfcf  23193  alexsublem  23195  tmdcn2  23240  tmdgsum  23246  tmdgsum2  23247  symgtgp  23257  subgntr  23258  opnsubg  23259  clssubg  23260  clsnsg  23261  cldsubg  23262  tgpconncompeqg  23263  tgpconncomp  23264  ghmcnp  23266  snclseqg  23267  tgphaus  23268  tgpt1  23269  prdstmdd  23275  prdstgpd  23276  tsmsgsum  23290  tsmsid  23291  tsmsmhm  23297  tsmsadd  23298  tgptsmscld  23302  utop3cls  23403  mopnuni  23594  isxms2  23601  prdsxmslem2  23685  metdseq0  24017  cnmpopc  24091  ishtpy  24135  om1val  24193  pi1val  24200  csscld  24413  clsocv  24414  cfilfcls  24438  relcmpcmet  24482  limcres  25050  limccnp  25055  limccnp2  25056  dvbss  25065  perfdvf  25067  dvreslem  25073  dvres2lem  25074  dvcnp2  25084  dvaddbr  25102  dvmulbr  25103  dvcmulf  25109  dvmptres2  25126  dvmptcmul  25128  dvmptntr  25135  dvcnvrelem2  25182  ftc1cn  25207  taylthlem1  25532  ulmdvlem3  25561  efrlim  26119  zart0  31829  zarmxt1  31830  pl1cn  31905  cvxpconn  33204  cvxsconn  33205  ivthALT  34524  neibastop2  34550  neibastop3  34551  topmeet  34553  topjoin  34554  refsum2cnlem1  42580  dvresntr  43459  rrxunitopnfi  43833