Theorem topontop 20718

Description: A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)

Assertion

Ref	Expression
topontop	|- ( J e. (TopOn ` B ) -> J e. Top )

Proof of Theorem topontop

Step	Hyp	Ref	Expression
1		istopon 20717	. 2 |- ( J e. (TopOn ` B ) <-> ( J e. Top /\ B = U. J ) )
2	1	simplbi 476	1 |- ( J e. (TopOn ` B ) -> J e. Top )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   U.cuni 4436   ` cfv 5888   Topctop 20698  TopOnctopon 20715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-topon 20716

This theorem is referenced by:  topontopi  20720  topontopon  20724  toprntopon  20729  toponmax  20730  topgele  20734  istps  20738  en2top  20789  pptbas  20812  toponmre  20897  cldmreon  20898  iscldtop  20899  neiptopreu  20937  resttopon  20965  resttopon2  20972  restlp  20987  restperf  20988  perfopn  20989  ordtopn3  21000  ordtcld1  21001  ordtcld2  21002  ordttop  21004  lmfval  21036  cnfval  21037  cnpfval  21038  tgcn  21056  tgcnp  21057  subbascn  21058  iscnp4  21067  iscncl  21073  cncls2  21077  cncls  21078  cnntr  21079  cncnp  21084  cnindis  21096  lmcls  21106  iscnrm2  21142  ist0-2  21148  ist1-2  21151  ishaus2  21155  hausnei2  21157  isreg2  21181  sscmp  21208  dfconn2  21222  clsconn  21233  conncompcld  21237  1stccnp  21265  locfincf  21334  kgenval  21338  kgenftop  21343  1stckgenlem  21356  kgen2ss  21358  txtopon  21394  pttopon  21399  txcls  21407  ptclsg  21418  dfac14lem  21420  xkoccn  21422  txcnp  21423  ptcnplem  21424  txlm  21451  cnmpt2res  21480  cnmptkp  21483  cnmptk1  21484  cnmpt1k  21485  cnmptkk  21486  cnmptk1p  21488  cnmptk2  21489  xkoinjcn  21490  qtoptopon  21507  qtopcld  21516  qtoprest  21520  qtopcmap  21522  kqval  21529  regr1lem  21542  kqreglem1  21544  kqreglem2  21545  kqnrmlem1  21546  kqnrmlem2  21547  kqtop  21548  pt1hmeo  21609  xpstopnlem1  21612  xkohmeo  21618  neifil  21684  trnei  21696  elflim  21775  flimss1  21777  flimopn  21779  fbflim2  21781  flimcf  21786  flimclslem  21788  flffval  21793  flfnei  21795  flftg  21800  cnpflf2  21804  isfcls2  21817  fclsopn  21818  fclsnei  21823  fclscf  21829  fclscmp  21834  fcfval  21837  fcfnei  21839  cnpfcf  21845  tgpmulg2  21898  tmdgsum  21899  tmdgsum2  21900  subgntr  21910  opnsubg  21911  clssubg  21912  clsnsg  21913  cldsubg  21914  snclseqg  21919  tgphaus  21920  qustgpopn  21923  prdstgpd  21928  tsmsgsum  21942  tsmsid  21943  tgptsmscld  21954  mopntop  22245  metdseq0  22657  cnmpt2pc  22727  ishtpy  22771  om1val  22830  pi1val  22837  csscld  23048  clsocv  23049  relcmpcmet  23115  bcth2  23127  limcres  23650  perfdvf  23667  dvaddbr  23701  dvmulbr  23702  dvcmulf  23708  dvmptres2  23725  dvmptcmul  23727  dvmptntr  23734  dvcnvlem  23739  lhop2  23778  lhop  23779  dvcnvrelem2  23781  taylthlem1  24127  neibastop2  32356  neibastop3  32357  topjoin  32360  dissneqlem  33187  istopclsd  37263  dvresntr  40132