Theorem topontop 22062

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

Step	Hyp	Ref	Expression
1		istopon 22061	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
2	1	simplbi 498	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  ∪ cuni 4839  ‘cfv 6433  Topctop 22042  TopOnctopon 22059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-topon 22060

This theorem is referenced by:  topontopi  22064  topontopon  22068  toprntopon  22074  toponmax  22075  topgele  22079  istps  22083  en2top  22135  pptbas  22158  toponmre  22244  cldmreon  22245  iscldtop  22246  neiptopreu  22284  resttopon  22312  resttopon2  22319  restlp  22334  restperf  22335  perfopn  22336  ordtopn3  22347  ordtcld1  22348  ordtcld2  22349  ordttop  22351  lmfval  22383  cnfval  22384  cnpfval  22385  tgcn  22403  tgcnp  22404  subbascn  22405  iscnp4  22414  iscncl  22420  cncls2  22424  cncls  22425  cnntr  22426  cncnp  22431  cnindis  22443  lmcls  22453  iscnrm2  22489  ist0-2  22495  ist1-2  22498  ishaus2  22502  hausnei2  22504  isreg2  22528  sscmp  22556  dfconn2  22570  clsconn  22581  conncompcld  22585  1stccnp  22613  locfincf  22682  kgenval  22686  kgenftop  22691  1stckgenlem  22704  kgen2ss  22706  txtopon  22742  pttopon  22747  txcls  22755  ptclsg  22766  dfac14lem  22768  xkoccn  22770  txcnp  22771  ptcnplem  22772  txlm  22799  cnmpt2res  22828  cnmptkp  22831  cnmptk1  22832  cnmpt1k  22833  cnmptkk  22834  cnmptk1p  22836  cnmptk2  22837  xkoinjcn  22838  qtoptopon  22855  qtopcld  22864  qtoprest  22868  qtopcmap  22870  kqval  22877  regr1lem  22890  kqreglem1  22892  kqreglem2  22893  kqnrmlem1  22894  kqnrmlem2  22895  kqtop  22896  pt1hmeo  22957  xpstopnlem1  22960  xkohmeo  22966  neifil  23031  trnei  23043  elflim  23122  flimss1  23124  flimopn  23126  fbflim2  23128  flimcf  23133  flimclslem  23135  flffval  23140  flfnei  23142  flftg  23147  cnpflf2  23151  isfcls2  23164  fclsopn  23165  fclsnei  23170  fclscf  23176  fclscmp  23181  fcfval  23184  fcfnei  23186  cnpfcf  23192  tgpmulg2  23245  tmdgsum  23246  tmdgsum2  23247  subgntr  23258  opnsubg  23259  clssubg  23260  clsnsg  23261  cldsubg  23262  snclseqg  23267  tgphaus  23268  qustgpopn  23271  prdstgpd  23276  tsmsgsum  23290  tsmsid  23291  tgptsmscld  23302  mopntop  23593  metdseq0  24017  cnmpopc  24091  ishtpy  24135  om1val  24193  pi1val  24200  csscld  24413  clsocv  24414  relcmpcmet  24482  bcth2  24494  limcres  25050  perfdvf  25067  dvaddbr  25102  dvmulbr  25103  dvcmulf  25109  dvmptres2  25126  dvmptcmul  25128  dvmptntr  25135  dvcnvlem  25140  lhop2  25179  lhop  25180  dvcnvrelem2  25182  taylthlem1  25532  zartop  31826  neibastop2  34550  neibastop3  34551  topjoin  34554  dissneqlem  35511  istopclsd  40522  dvresntr  43459