Theorem toponuni 23108

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ∪ cuni 4877  ‘cfv 6543  Topctop 23087  TopOnctopon 23104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fv 6551  df-topon 23105

This theorem is used by:  toponunii  23110  toponmax  23120  toponss  23121  toponcom  23122  topgele  23124  topontopn  23134  toponmre  23287  cldmreon  23288  restuni  23356  resttopon2  23362  restlp  23377  restperf  23378  perfopn  23379  ordtcld1  23391  ordtcld2  23392  lmfval  23426  cnfval  23427  cnpfval  23428  cnpf2  23444  cnprcl2  23445  ssidcn  23449  iscnp4  23457  iscncl  23463  cncls2  23467  cncls  23468  cnntr  23469  cncnp  23474  lmcls  23496  lmcld  23497  iscnrm2  23532  ist0-2  23538  ist1-2  23541  ishaus2  23545  isreg2  23571  ordtt1  23573  sscmp  23599  dfconn2  23613  clsconn  23624  conncompcld  23628  1stccnp  23656  locfincf  23725  kgenval  23729  kgenuni  23733  1stckgenlem  23747  kgen2ss  23749  kgencn2  23751  txtopon  23785  txuni  23786  pttopon  23790  ptuniconst  23792  txcls  23798  ptclsg  23809  dfac14lem  23811  xkoccn  23813  ptcnplem  23815  ptcn  23821  cnmpt1t  23859  cnmpt2t  23867  cnmpt1res  23870  cnmpt2res  23871  cnmptkp  23874  cnmptk1p  23879  cnmptk2  23880  xkoinjcn  23881  elqtop3  23897  qtoptopon  23898  qtopcld  23907  qtoprest  23911  qtopcmap  23913  kqval  23920  kqcldsat  23927  isr0  23931  r0cld  23932  regr1lem  23933  kqnrmlem1  23937  kqnrmlem2  23938  pt1hmeo  24000  xpstopnlem1  24003  neifil  24074  trnei  24086  elflim  24165  flimss2  24166  flimss1  24167  flimopn  24169  fbflim2  24171  flimclslem  24178  flffval  24183  flfnei  24185  cnpflf2  24194  cnflf  24196  cnflf2  24197  isfcls2  24207  fclsopn  24208  fclsnei  24213  fclscmp  24224  ufilcmp  24226  fcfval  24227  fcfnei  24229  fcfelbas  24230  cnpfcf  24235  cnfcf  24236  alexsublem  24238  tmdcn2  24283  tmdgsum  24289  tmdgsum2  24290  symgtgp  24300  subgntr  24301  opnsubg  24302  clssubg  24303  clsnsg  24304  cldsubg  24305  tgpconncompeqg  24306  tgpconncomp  24307  ghmcnp  24309  snclseqg  24310  tgphaus  24311  tgpt1  24312  prdstmdd  24318  prdstgpd  24319  tsmsgsum  24333  tsmsid  24334  tsmsmhm  24340  tsmsadd  24341  tgptsmscld  24345  utop3cls  24445  mopnuni  24635  isxms2  24642  prdsxmslem2  24723  metdseq0  25049  cnmpopc  25124  ishtpy  25168  om1val  25226  pi1val  25233  csscld  25445  clsocv  25446  cfilfcls  25470  relcmpcmet  25514  limcres  26082  limccnp  26087  limccnp2  26088  dvbss  26097  perfdvf  26099  dvreslem  26105  dvres2lem  26106  dvcnp2  26116  dvaddbr  26134  dvmulbr  26135  dvcmulf  26141  dvmptres2  26158  dvmptcmul  26160  dvmptntr  26167  dvcnvrelem2  26214  ftc1cn  26239  taylthlem1  26573  ulmdvlem3  26602  efrlim  27171  zart0  34300  zarmxt1  34301  pl1cn  34376  cvxpconn  35755  cvxsconn  35756  ivthALT  36887  neibastop2  36913  neibastop3  36914  topmeet  36916  topjoin  36917  refsum2cnlem1  45798  dvresntr  46673  rrxunitopnfi  47047