Theorem toponmax 22901

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 22889	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 22888	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2737	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 22881	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 17	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2837	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2114  ∪ cuni 4851  ‘cfv 6492  Topctop 22868  TopOnctopon 22885

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 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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-top 22869  df-topon 22886

This theorem is referenced by:  topgele  22905  eltpsg  22918  en2top  22960  resttopon  23136  ordtrest  23177  ordtrest2lem  23178  ordtrest2  23179  lmfval  23207  cnpfval  23209  iscn  23210  iscnp  23212  lmbrf  23235  cncls  23249  cnconst2  23258  cnrest2  23261  cndis  23266  cnindis  23267  cnpdis  23268  lmfss  23271  lmres  23275  lmff  23276  ist1-3  23324  connsuba  23395  unconn  23404  kgenval  23510  elkgen  23511  kgentopon  23513  pttoponconst  23572  tx1cn  23584  tx2cn  23585  ptcls  23591  xkoccn  23594  txlm  23623  cnmpt2res  23652  xkoinjcn  23662  qtoprest  23692  ordthmeolem  23776  pt1hmeo  23781  xkocnv  23789  flimclslem  23959  flfval  23965  flfnei  23966  isflf  23968  flfcnp  23979  txflf  23981  supnfcls  23995  fclscf  24000  fclscmp  24005  fcfval  24008  isfcf  24009  uffcfflf  24014  cnpfcf  24016  mopnm  24419  isxms2  24423  prdsxmslem2  24504  bcth2  25307  dvmptid  25934  dvmptc  25935  dvtaylp  26347  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  pige3ALT  26497  dvcxp1  26717  cxpcn3  26725  ordtrestNEW  34081  ordtrest2NEWlem  34082  ordtrest2NEW  34083  topjoin  36563  areacirclem1  38043