Theorem toponmax 22842

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 22830	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 22829	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2733	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 22822	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 17	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2833	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2113  ∪ cuni 4858  ‘cfv 6486  Topctop 22809  TopOnctopon 22826

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6442  df-fun 6488  df-fv 6494  df-top 22810  df-topon 22827

This theorem is referenced by:  topgele  22846  eltpsg  22859  en2top  22901  resttopon  23077  ordtrest  23118  ordtrest2lem  23119  ordtrest2  23120  lmfval  23148  cnpfval  23150  iscn  23151  iscnp  23153  lmbrf  23176  cncls  23190  cnconst2  23199  cnrest2  23202  cndis  23207  cnindis  23208  cnpdis  23209  lmfss  23212  lmres  23216  lmff  23217  ist1-3  23265  connsuba  23336  unconn  23345  kgenval  23451  elkgen  23452  kgentopon  23454  pttoponconst  23513  tx1cn  23525  tx2cn  23526  ptcls  23532  xkoccn  23535  txlm  23564  cnmpt2res  23593  xkoinjcn  23603  qtoprest  23633  ordthmeolem  23717  pt1hmeo  23722  xkocnv  23730  flimclslem  23900  flfval  23906  flfnei  23907  isflf  23909  flfcnp  23920  txflf  23922  supnfcls  23936  fclscf  23941  fclscmp  23946  fcfval  23949  isfcf  23950  uffcfflf  23955  cnpfcf  23957  mopnm  24360  isxms2  24364  prdsxmslem2  24445  bcth2  25258  dvmptid  25889  dvmptc  25890  dvtaylp  26306  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  pige3ALT  26457  dvcxp1  26677  cxpcn3  26686  ordtrestNEW  33955  ordtrest2NEWlem  33956  ordtrest2NEW  33957  topjoin  36430  areacirclem1  37768