Theorem toponmax 21531

Description: The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.)

Assertion

Ref	Expression
toponmax	⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

Proof of Theorem toponmax

Step	Hyp	Ref	Expression
1		toponuni 21519	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 21518	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2798	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 21511	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 17	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2890	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2111  ∪ cuni 4800  ‘cfv 6324  Topctop 21498  TopOnctopon 21515

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-iota 6283  df-fun 6326  df-fv 6332  df-top 21499  df-topon 21516

This theorem is referenced by:  topgele  21535  eltpsg  21548  en2top  21590  resttopon  21766  ordtrest  21807  ordtrest2lem  21808  ordtrest2  21809  lmfval  21837  cnpfval  21839  iscn  21840  iscnp  21842  lmbrf  21865  cncls  21879  cnconst2  21888  cnrest2  21891  cndis  21896  cnindis  21897  cnpdis  21898  lmfss  21901  lmres  21905  lmff  21906  ist1-3  21954  connsuba  22025  unconn  22034  kgenval  22140  elkgen  22141  kgentopon  22143  pttoponconst  22202  tx1cn  22214  tx2cn  22215  ptcls  22221  xkoccn  22224  txlm  22253  cnmpt2res  22282  xkoinjcn  22292  qtoprest  22322  ordthmeolem  22406  pt1hmeo  22411  xkocnv  22419  flimclslem  22589  flfval  22595  flfnei  22596  isflf  22598  flfcnp  22609  txflf  22611  supnfcls  22625  fclscf  22630  fclscmp  22635  fcfval  22638  isfcf  22639  uffcfflf  22644  cnpfcf  22646  mopnm  23051  isxms2  23055  prdsxmslem2  23136  bcth2  23934  dvmptid  24560  dvmptc  24561  dvtaylp  24965  taylthlem1  24968  taylthlem2  24969  pige3ALT  25112  dvcxp1  25329  cxpcn3  25337  ordtrestNEW  31274  ordtrest2NEWlem  31275  ordtrest2NEW  31276  topjoin  33826  areacirclem1  35145