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

Theorem topontop 20766
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 20765 . 2 (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = 𝐽))
21simplbi 475 1 (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030   cuni 4468  cfv 5926  Topctop 20746  TopOnctopon 20763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fv 5934  df-topon 20764
This theorem is referenced by:  topontopi  20768  topontopon  20772  toprntopon  20777  toponmax  20778  topgele  20782  istps  20786  en2top  20837  pptbas  20860  toponmre  20945  cldmreon  20946  iscldtop  20947  neiptopreu  20985  resttopon  21013  resttopon2  21020  restlp  21035  restperf  21036  perfopn  21037  ordtopn3  21048  ordtcld1  21049  ordtcld2  21050  ordttop  21052  lmfval  21084  cnfval  21085  cnpfval  21086  tgcn  21104  tgcnp  21105  subbascn  21106  iscnp4  21115  iscncl  21121  cncls2  21125  cncls  21126  cnntr  21127  cncnp  21132  cnindis  21144  lmcls  21154  iscnrm2  21190  ist0-2  21196  ist1-2  21199  ishaus2  21203  hausnei2  21205  isreg2  21229  sscmp  21256  dfconn2  21270  clsconn  21281  conncompcld  21285  1stccnp  21313  locfincf  21382  kgenval  21386  kgenftop  21391  1stckgenlem  21404  kgen2ss  21406  txtopon  21442  pttopon  21447  txcls  21455  ptclsg  21466  dfac14lem  21468  xkoccn  21470  txcnp  21471  ptcnplem  21472  txlm  21499  cnmpt2res  21528  cnmptkp  21531  cnmptk1  21532  cnmpt1k  21533  cnmptkk  21534  cnmptk1p  21536  cnmptk2  21537  xkoinjcn  21538  qtoptopon  21555  qtopcld  21564  qtoprest  21568  qtopcmap  21570  kqval  21577  regr1lem  21590  kqreglem1  21592  kqreglem2  21593  kqnrmlem1  21594  kqnrmlem2  21595  kqtop  21596  pt1hmeo  21657  xpstopnlem1  21660  xkohmeo  21666  neifil  21731  trnei  21743  elflim  21822  flimss1  21824  flimopn  21826  fbflim2  21828  flimcf  21833  flimclslem  21835  flffval  21840  flfnei  21842  flftg  21847  cnpflf2  21851  isfcls2  21864  fclsopn  21865  fclsnei  21870  fclscf  21876  fclscmp  21881  fcfval  21884  fcfnei  21886  cnpfcf  21892  tgpmulg2  21945  tmdgsum  21946  tmdgsum2  21947  subgntr  21957  opnsubg  21958  clssubg  21959  clsnsg  21960  cldsubg  21961  snclseqg  21966  tgphaus  21967  qustgpopn  21970  prdstgpd  21975  tsmsgsum  21989  tsmsid  21990  tgptsmscld  22001  mopntop  22292  metdseq0  22704  cnmpt2pc  22774  ishtpy  22818  om1val  22876  pi1val  22883  csscld  23094  clsocv  23095  relcmpcmet  23161  bcth2  23173  limcres  23695  perfdvf  23712  dvaddbr  23746  dvmulbr  23747  dvcmulf  23753  dvmptres2  23770  dvmptcmul  23772  dvmptntr  23779  dvcnvlem  23784  lhop2  23823  lhop  23824  dvcnvrelem2  23826  taylthlem1  24172  neibastop2  32481  neibastop3  32482  topjoin  32485  dissneqlem  33317  istopclsd  37580  dvresntr  40450
  Copyright terms: Public domain W3C validator