Theorem toponmax 22829

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 22817	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 22816	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2729	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 22809	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 17	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2828	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2109  ∪ cuni 4861  ‘cfv 6486  Topctop 22796  TopOnctopon 22813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494  df-top 22797  df-topon 22814

This theorem is referenced by:  topgele  22833  eltpsg  22846  en2top  22888  resttopon  23064  ordtrest  23105  ordtrest2lem  23106  ordtrest2  23107  lmfval  23135  cnpfval  23137  iscn  23138  iscnp  23140  lmbrf  23163  cncls  23177  cnconst2  23186  cnrest2  23189  cndis  23194  cnindis  23195  cnpdis  23196  lmfss  23199  lmres  23203  lmff  23204  ist1-3  23252  connsuba  23323  unconn  23332  kgenval  23438  elkgen  23439  kgentopon  23441  pttoponconst  23500  tx1cn  23512  tx2cn  23513  ptcls  23519  xkoccn  23522  txlm  23551  cnmpt2res  23580  xkoinjcn  23590  qtoprest  23620  ordthmeolem  23704  pt1hmeo  23709  xkocnv  23717  flimclslem  23887  flfval  23893  flfnei  23894  isflf  23896  flfcnp  23907  txflf  23909  supnfcls  23923  fclscf  23928  fclscmp  23933  fcfval  23936  isfcf  23937  uffcfflf  23942  cnpfcf  23944  mopnm  24348  isxms2  24352  prdsxmslem2  24433  bcth2  25246  dvmptid  25877  dvmptc  25878  dvtaylp  26294  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  pige3ALT  26445  dvcxp1  26665  cxpcn3  26674  ordtrestNEW  33887  ordtrest2NEWlem  33888  ordtrest2NEW  33889  topjoin  36338  areacirclem1  37687