Theorem toponmax 22882

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∪ cuni 4865  ‘cfv 6500  Topctop 22849  TopOnctopon 22866

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-top 22850  df-topon 22867

This theorem is referenced by:  topgele  22886  eltpsg  22899  en2top  22941  resttopon  23117  ordtrest  23158  ordtrest2lem  23159  ordtrest2  23160  lmfval  23188  cnpfval  23190  iscn  23191  iscnp  23193  lmbrf  23216  cncls  23230  cnconst2  23239  cnrest2  23242  cndis  23247  cnindis  23248  cnpdis  23249  lmfss  23252  lmres  23256  lmff  23257  ist1-3  23305  connsuba  23376  unconn  23385  kgenval  23491  elkgen  23492  kgentopon  23494  pttoponconst  23553  tx1cn  23565  tx2cn  23566  ptcls  23572  xkoccn  23575  txlm  23604  cnmpt2res  23633  xkoinjcn  23643  qtoprest  23673  ordthmeolem  23757  pt1hmeo  23762  xkocnv  23770  flimclslem  23940  flfval  23946  flfnei  23947  isflf  23949  flfcnp  23960  txflf  23962  supnfcls  23976  fclscf  23981  fclscmp  23986  fcfval  23989  isfcf  23990  uffcfflf  23995  cnpfcf  23997  mopnm  24400  isxms2  24404  prdsxmslem2  24485  bcth2  25298  dvmptid  25929  dvmptc  25930  dvtaylp  26346  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  pige3ALT  26497  dvcxp1  26717  cxpcn3  26726  ordtrestNEW  34098  ordtrest2NEWlem  34099  ordtrest2NEW  34100  topjoin  36578  areacirclem1  37953