Theorem topontop 22857

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∪ cuni 4863  ‘cfv 6492  Topctop 22837  TopOnctopon 22854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  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 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-topon 22855

This theorem is referenced by:  topontopi  22859  topontopon  22863  toprntopon  22869  toponmax  22870  topgele  22874  istps  22878  en2top  22929  pptbas  22952  toponmre  23037  cldmreon  23038  iscldtop  23039  neiptopreu  23077  resttopon  23105  resttopon2  23112  restlp  23127  restperf  23128  perfopn  23129  ordtopn3  23140  ordtcld1  23141  ordtcld2  23142  ordttop  23144  lmfval  23176  cnfval  23177  cnpfval  23178  tgcn  23196  tgcnp  23197  subbascn  23198  iscnp4  23207  iscncl  23213  cncls2  23217  cncls  23218  cnntr  23219  cncnp  23224  cnindis  23236  lmcls  23246  iscnrm2  23282  ist0-2  23288  ist1-2  23291  ishaus2  23295  hausnei2  23297  isreg2  23321  sscmp  23349  dfconn2  23363  clsconn  23374  conncompcld  23378  1stccnp  23406  locfincf  23475  kgenval  23479  kgenftop  23484  1stckgenlem  23497  kgen2ss  23499  txtopon  23535  pttopon  23540  txcls  23548  ptclsg  23559  dfac14lem  23561  xkoccn  23563  txcnp  23564  ptcnplem  23565  txlm  23592  cnmpt2res  23621  cnmptkp  23624  cnmptk1  23625  cnmpt1k  23626  cnmptkk  23627  cnmptk1p  23629  cnmptk2  23630  xkoinjcn  23631  qtoptopon  23648  qtopcld  23657  qtoprest  23661  qtopcmap  23663  kqval  23670  regr1lem  23683  kqreglem1  23685  kqreglem2  23686  kqnrmlem1  23687  kqnrmlem2  23688  kqtop  23689  pt1hmeo  23750  xpstopnlem1  23753  xkohmeo  23759  neifil  23824  trnei  23836  elflim  23915  flimss1  23917  flimopn  23919  fbflim2  23921  flimcf  23926  flimclslem  23928  flffval  23933  flfnei  23935  flftg  23940  cnpflf2  23944  isfcls2  23957  fclsopn  23958  fclsnei  23963  fclscf  23969  fclscmp  23974  fcfval  23977  fcfnei  23979  cnpfcf  23985  tgpmulg2  24038  tmdgsum  24039  tmdgsum2  24040  subgntr  24051  opnsubg  24052  clssubg  24053  clsnsg  24054  cldsubg  24055  snclseqg  24060  tgphaus  24061  qustgpopn  24064  prdstgpd  24069  tsmsgsum  24083  tsmsid  24084  tgptsmscld  24095  mopntop  24384  metdseq0  24799  cnmpopc  24878  ishtpy  24927  om1val  24986  pi1val  24993  csscld  25205  clsocv  25206  relcmpcmet  25274  bcth2  25286  limcres  25843  perfdvf  25860  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvcmulf  25904  dvmptres2  25922  dvmptcmul  25924  dvmptntr  25931  dvcnvlem  25936  lhop2  25976  lhop  25977  dvcnvrelem2  25979  taylthlem1  26337  zartop  34033  neibastop2  36555  neibastop3  36556  topjoin  36559  dissneqlem  37545  istopclsd  42952  dvresntr  46172