Theorem toponuni 22879

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∪ cuni 4850  ‘cfv 6498  Topctop 22858  TopOnctopon 22875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506  df-topon 22876

This theorem is referenced by:  toponunii  22881  toponmax  22891  toponss  22892  toponcom  22893  topgele  22895  topontopn  22905  toponmre  23058  cldmreon  23059  restuni  23127  resttopon2  23133  restlp  23148  restperf  23149  perfopn  23150  ordtcld1  23162  ordtcld2  23163  lmfval  23197  cnfval  23198  cnpfval  23199  cnpf2  23215  cnprcl2  23216  ssidcn  23220  iscnp4  23228  iscncl  23234  cncls2  23238  cncls  23239  cnntr  23240  cncnp  23245  lmcls  23267  lmcld  23268  iscnrm2  23303  ist0-2  23309  ist1-2  23312  ishaus2  23316  isreg2  23342  ordtt1  23344  sscmp  23370  dfconn2  23384  clsconn  23395  conncompcld  23399  1stccnp  23427  locfincf  23496  kgenval  23500  kgenuni  23504  1stckgenlem  23518  kgen2ss  23520  kgencn2  23522  txtopon  23556  txuni  23557  pttopon  23561  ptuniconst  23563  txcls  23569  ptclsg  23580  dfac14lem  23582  xkoccn  23584  ptcnplem  23586  ptcn  23592  cnmpt1t  23630  cnmpt2t  23638  cnmpt1res  23641  cnmpt2res  23642  cnmptkp  23645  cnmptk1p  23650  cnmptk2  23651  xkoinjcn  23652  elqtop3  23668  qtoptopon  23669  qtopcld  23678  qtoprest  23682  qtopcmap  23684  kqval  23691  kqcldsat  23698  isr0  23702  r0cld  23703  regr1lem  23704  kqnrmlem1  23708  kqnrmlem2  23709  pt1hmeo  23771  xpstopnlem1  23774  neifil  23845  trnei  23857  elflim  23936  flimss2  23937  flimss1  23938  flimopn  23940  fbflim2  23942  flimclslem  23949  flffval  23954  flfnei  23956  cnpflf2  23965  cnflf  23967  cnflf2  23968  isfcls2  23978  fclsopn  23979  fclsnei  23984  fclscmp  23995  ufilcmp  23997  fcfval  23998  fcfnei  24000  fcfelbas  24001  cnpfcf  24006  cnfcf  24007  alexsublem  24009  tmdcn2  24054  tmdgsum  24060  tmdgsum2  24061  symgtgp  24071  subgntr  24072  opnsubg  24073  clssubg  24074  clsnsg  24075  cldsubg  24076  tgpconncompeqg  24077  tgpconncomp  24078  ghmcnp  24080  snclseqg  24081  tgphaus  24082  tgpt1  24083  prdstmdd  24089  prdstgpd  24090  tsmsgsum  24104  tsmsid  24105  tsmsmhm  24111  tsmsadd  24112  tgptsmscld  24116  utop3cls  24216  mopnuni  24406  isxms2  24413  prdsxmslem2  24494  metdseq0  24820  cnmpopc  24895  ishtpy  24939  om1val  24997  pi1val  25004  csscld  25216  clsocv  25217  cfilfcls  25241  relcmpcmet  25285  limcres  25853  limccnp  25858  limccnp2  25859  dvbss  25868  perfdvf  25870  dvreslem  25876  dvres2lem  25877  dvcnp2  25887  dvaddbr  25905  dvmulbr  25906  dvcmulf  25912  dvmptres2  25929  dvmptcmul  25931  dvmptntr  25938  dvcnvrelem2  25985  ftc1cn  26010  taylthlem1  26338  ulmdvlem3  26367  efrlim  26933  zart0  34023  zarmxt1  34024  pl1cn  34099  cvxpconn  35424  cvxsconn  35425  ivthALT  36517  neibastop2  36543  neibastop3  36544  topmeet  36546  topjoin  36547  refsum2cnlem1  45468  dvresntr  46346  rrxunitopnfi  46720