Theorem topontop 22878

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 22877	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
2	1	simplbi 496	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∪ cuni 4850  ‘cfv 6498  Topctop 22858  TopOnctopon 22875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506  df-topon 22876

This theorem is referenced by:  topontopi  22880  topontopon  22884  toprntopon  22890  toponmax  22891  topgele  22895  istps  22899  en2top  22950  pptbas  22973  toponmre  23058  cldmreon  23059  iscldtop  23060  neiptopreu  23098  resttopon  23126  resttopon2  23133  restlp  23148  restperf  23149  perfopn  23150  ordtopn3  23161  ordtcld1  23162  ordtcld2  23163  ordttop  23165  lmfval  23197  cnfval  23198  cnpfval  23199  tgcn  23217  tgcnp  23218  subbascn  23219  iscnp4  23228  iscncl  23234  cncls2  23238  cncls  23239  cnntr  23240  cncnp  23245  cnindis  23257  lmcls  23267  iscnrm2  23303  ist0-2  23309  ist1-2  23312  ishaus2  23316  hausnei2  23318  isreg2  23342  sscmp  23370  dfconn2  23384  clsconn  23395  conncompcld  23399  1stccnp  23427  locfincf  23496  kgenval  23500  kgenftop  23505  1stckgenlem  23518  kgen2ss  23520  txtopon  23556  pttopon  23561  txcls  23569  ptclsg  23580  dfac14lem  23582  xkoccn  23584  txcnp  23585  ptcnplem  23586  txlm  23613  cnmpt2res  23642  cnmptkp  23645  cnmptk1  23646  cnmpt1k  23647  cnmptkk  23648  cnmptk1p  23650  cnmptk2  23651  xkoinjcn  23652  qtoptopon  23669  qtopcld  23678  qtoprest  23682  qtopcmap  23684  kqval  23691  regr1lem  23704  kqreglem1  23706  kqreglem2  23707  kqnrmlem1  23708  kqnrmlem2  23709  kqtop  23710  pt1hmeo  23771  xpstopnlem1  23774  xkohmeo  23780  neifil  23845  trnei  23857  elflim  23936  flimss1  23938  flimopn  23940  fbflim2  23942  flimcf  23947  flimclslem  23949  flffval  23954  flfnei  23956  flftg  23961  cnpflf2  23965  isfcls2  23978  fclsopn  23979  fclsnei  23984  fclscf  23990  fclscmp  23995  fcfval  23998  fcfnei  24000  cnpfcf  24006  tgpmulg2  24059  tmdgsum  24060  tmdgsum2  24061  subgntr  24072  opnsubg  24073  clssubg  24074  clsnsg  24075  cldsubg  24076  snclseqg  24081  tgphaus  24082  qustgpopn  24085  prdstgpd  24090  tsmsgsum  24104  tsmsid  24105  tgptsmscld  24116  mopntop  24405  metdseq0  24820  cnmpopc  24895  ishtpy  24939  om1val  24997  pi1val  25004  csscld  25216  clsocv  25217  relcmpcmet  25285  bcth2  25297  limcres  25853  perfdvf  25870  dvaddbr  25905  dvmulbr  25906  dvcmulf  25912  dvmptres2  25929  dvmptcmul  25931  dvmptntr  25938  dvcnvlem  25943  lhop2  25982  lhop  25983  dvcnvrelem2  25985  taylthlem1  26338  zartop  34020  neibastop2  36543  neibastop3  36544  topjoin  36547  dissneqlem  37656  istopclsd  43132  dvresntr  46346