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

Theorem topontop 20641
Description: A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
topontop (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)

Proof of Theorem topontop
StepHypRef Expression
1 istopon 20640 . 2 (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = 𝐽))
21simplbi 476 1 (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987   cuni 4402  cfv 5847  Topctop 20617  TopOnctopon 20618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-iota 5810  df-fun 5849  df-fv 5855  df-topon 20623
This theorem is referenced by:  toponmax  20643  topontopi  20646  topgele  20649  istps  20651  en2top  20700  pptbas  20722  toponmre  20807  cldmreon  20808  iscldtop  20809  neiptopreu  20847  resttopon  20875  resttopon2  20882  restlp  20897  restperf  20898  perfopn  20899  ordtopn3  20910  ordtcld1  20911  ordtcld2  20912  ordttop  20914  lmfval  20946  cnfval  20947  cnpfval  20948  tgcn  20966  tgcnp  20967  subbascn  20968  iscnp4  20977  iscncl  20983  cncls2  20987  cncls  20988  cnntr  20989  cncnp  20994  cnindis  21006  lmcls  21016  iscnrm2  21052  ist0-2  21058  ist1-2  21061  ishaus2  21065  hausnei2  21067  isreg2  21091  sscmp  21118  dfconn2  21132  clsconn  21143  conncompcld  21147  1stccnp  21175  locfincf  21244  kgenval  21248  kgenftop  21253  1stckgenlem  21266  kgen2ss  21268  txtopon  21304  pttopon  21309  txcls  21317  ptclsg  21328  dfac14lem  21330  xkoccn  21332  txcnp  21333  ptcnplem  21334  txlm  21361  cnmpt2res  21390  cnmptkp  21393  cnmptk1  21394  cnmpt1k  21395  cnmptkk  21396  cnmptk1p  21398  cnmptk2  21399  xkoinjcn  21400  qtoptopon  21417  qtopcld  21426  qtoprest  21430  qtopcmap  21432  kqval  21439  regr1lem  21452  kqreglem1  21454  kqreglem2  21455  kqnrmlem1  21456  kqnrmlem2  21457  kqtop  21458  pt1hmeo  21519  xpstopnlem1  21522  xkohmeo  21528  neifil  21594  trnei  21606  elflim  21685  flimss1  21687  flimopn  21689  fbflim2  21691  flimcf  21696  flimclslem  21698  flffval  21703  flfnei  21705  flftg  21710  cnpflf2  21714  isfcls2  21727  fclsopn  21728  fclsnei  21733  fclscf  21739  fclscmp  21744  fcfval  21747  fcfnei  21749  cnpfcf  21755  tgpmulg2  21808  tmdgsum  21809  tmdgsum2  21810  subgntr  21820  opnsubg  21821  clssubg  21822  clsnsg  21823  cldsubg  21824  snclseqg  21829  tgphaus  21830  qustgpopn  21833  prdstgpd  21838  tsmsgsum  21852  tsmsid  21853  tgptsmscld  21864  mopntop  22155  metdseq0  22565  cnmpt2pc  22635  ishtpy  22679  om1val  22738  pi1val  22745  csscld  22956  clsocv  22957  relcmpcmet  23023  bcth2  23035  limcres  23556  perfdvf  23573  dvaddbr  23607  dvmulbr  23608  dvcmulf  23614  dvmptres2  23631  dvmptcmul  23633  dvmptntr  23640  dvcnvlem  23643  lhop2  23682  lhop  23683  dvcnvrelem2  23685  taylthlem1  24031  neibastop2  31998  neibastop3  31999  topjoin  32002  bj-topontopon  32691  bj-toprntopon  32700  dissneqlem  32819  istopclsd  36743  dvresntr  39437
  Copyright terms: Public domain W3C validator