MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  toponuni Structured version   Visualization version   GIF version

Theorem toponuni 20936
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
StepHypRef Expression
1 istopon 20934 . 2 (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = 𝐽))
21simprbi 486 1 (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = 𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2157   cuni 4637  cfv 6104  Topctop 20915  TopOnctopon 20932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-opab 4914  df-mpt 4931  df-id 5226  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-iota 6067  df-fun 6106  df-fv 6112  df-topon 20933
This theorem is referenced by:  toponunii  20938  toponmax  20948  toponss  20949  toponcom  20950  topgele  20952  topontopn  20962  toponmre  21115  cldmreon  21116  restuni  21184  resttopon2  21190  restlp  21205  restperf  21206  perfopn  21207  ordtcld1  21219  ordtcld2  21220  lmfval  21254  cnfval  21255  cnpfval  21256  cnpf2  21272  cnprcl2  21273  ssidcn  21277  iscnp4  21285  iscncl  21291  cncls2  21295  cncls  21296  cnntr  21297  cncnp  21302  lmcls  21324  lmcld  21325  iscnrm2  21360  ist0-2  21366  ist1-2  21369  ishaus2  21373  isreg2  21399  ordtt1  21401  sscmp  21426  dfconn2  21440  clsconn  21451  conncompcld  21455  1stccnp  21483  locfincf  21552  kgenval  21556  kgenuni  21560  1stckgenlem  21574  kgen2ss  21576  kgencn2  21578  txtopon  21612  txuni  21613  pttopon  21617  ptuniconst  21619  txcls  21625  ptclsg  21636  dfac14lem  21638  xkoccn  21640  ptcnplem  21642  ptcn  21648  cnmpt1t  21686  cnmpt2t  21694  cnmpt1res  21697  cnmpt2res  21698  cnmptkp  21701  cnmptk1p  21706  cnmptk2  21707  xkoinjcn  21708  elqtop3  21724  qtoptopon  21725  qtopcld  21734  qtoprest  21738  qtopcmap  21740  kqval  21747  kqcldsat  21754  isr0  21758  r0cld  21759  regr1lem  21760  kqnrmlem1  21764  kqnrmlem2  21765  pt1hmeo  21827  xpstopnlem1  21830  neifil  21901  trnei  21913  elflim  21992  flimss2  21993  flimss1  21994  flimopn  21996  fbflim2  21998  flimclslem  22005  flffval  22010  flfnei  22012  cnpflf2  22021  cnflf  22023  cnflf2  22024  isfcls2  22034  fclsopn  22035  fclsnei  22040  fclscmp  22051  ufilcmp  22053  fcfval  22054  fcfnei  22056  fcfelbas  22057  cnpfcf  22062  cnfcf  22063  alexsublem  22065  tmdcn2  22110  tmdgsum  22116  tmdgsum2  22117  symgtgp  22122  subgntr  22127  opnsubg  22128  clssubg  22129  clsnsg  22130  cldsubg  22131  tgpconncompeqg  22132  tgpconncomp  22133  ghmcnp  22135  snclseqg  22136  tgphaus  22137  tgpt1  22138  prdstmdd  22144  prdstgpd  22145  tsmsgsum  22159  tsmsid  22160  tsmsmhm  22166  tsmsadd  22167  tgptsmscld  22171  utop3cls  22272  mopnuni  22463  isxms2  22470  prdsxmslem2  22551  metdseq0  22874  cnmpt2pc  22944  ishtpy  22988  om1val  23046  pi1val  23053  csscld  23264  clsocv  23265  cfilfcls  23289  relcmpcmet  23332  limcres  23870  limccnp  23875  limccnp2  23876  dvbss  23885  perfdvf  23887  dvreslem  23893  dvres2lem  23894  dvcnp2  23903  dvaddbr  23921  dvmulbr  23922  dvcmulf  23928  dvmptres2  23945  dvmptcmul  23947  dvmptntr  23954  dvcnvrelem2  24001  ftc1cn  24026  taylthlem1  24347  ulmdvlem3  24376  efrlim  24916  pl1cn  30332  cvxpconn  31552  cvxsconn  31553  ivthALT  32656  neibastop2  32682  neibastop3  32683  topmeet  32685  topjoin  32686  refsum2cnlem1  39691  dvresntr  40613  rrxunitopnfi  40992
  Copyright terms: Public domain W3C validator