Theorem toponmax 22312

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 22300	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 22299	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2731	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 22292	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 17	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2832	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2106  ∪ cuni 4870  ‘cfv 6501  Topctop 22279  TopOnctopon 22296

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6453  df-fun 6503  df-fv 6509  df-top 22280  df-topon 22297

This theorem is referenced by:  topgele  22316  eltpsg  22329  eltpsgOLD  22330  en2top  22372  resttopon  22549  ordtrest  22590  ordtrest2lem  22591  ordtrest2  22592  lmfval  22620  cnpfval  22622  iscn  22623  iscnp  22625  lmbrf  22648  cncls  22662  cnconst2  22671  cnrest2  22674  cndis  22679  cnindis  22680  cnpdis  22681  lmfss  22684  lmres  22688  lmff  22689  ist1-3  22737  connsuba  22808  unconn  22817  kgenval  22923  elkgen  22924  kgentopon  22926  pttoponconst  22985  tx1cn  22997  tx2cn  22998  ptcls  23004  xkoccn  23007  txlm  23036  cnmpt2res  23065  xkoinjcn  23075  qtoprest  23105  ordthmeolem  23189  pt1hmeo  23194  xkocnv  23202  flimclslem  23372  flfval  23378  flfnei  23379  isflf  23381  flfcnp  23392  txflf  23394  supnfcls  23408  fclscf  23413  fclscmp  23418  fcfval  23421  isfcf  23422  uffcfflf  23427  cnpfcf  23429  mopnm  23834  isxms2  23838  prdsxmslem2  23922  bcth2  24731  dvmptid  25358  dvmptc  25359  dvtaylp  25766  taylthlem1  25769  taylthlem2  25770  pige3ALT  25913  dvcxp1  26130  cxpcn3  26138  ordtrestNEW  32591  ordtrest2NEWlem  32592  ordtrest2NEW  32593  topjoin  34913  areacirclem1  36239