Theorem toponmax 20951

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 20939	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 20938	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2771	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 20931	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 17	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2850	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2145  ∪ cuni 4574  ‘cfv 6031  Topctop 20918  TopOnctopon 20935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fv 6039  df-top 20919  df-topon 20936

This theorem is referenced by:  topgele  20955  eltpsg  20968  en2top  21010  resttopon  21186  ordtrest  21227  ordtrest2lem  21228  ordtrest2  21229  lmfval  21257  cnpfval  21259  iscn  21260  iscnp  21262  lmbrf  21285  cncls  21299  cnconst2  21308  cnrest2  21311  cndis  21316  cnindis  21317  cnpdis  21318  lmfss  21321  lmres  21325  lmff  21326  ist1-3  21374  connsuba  21444  unconn  21453  kgenval  21559  elkgen  21560  kgentopon  21562  pttoponconst  21621  tx1cn  21633  tx2cn  21634  ptcls  21640  xkoccn  21643  txlm  21672  cnmpt2res  21701  xkoinjcn  21711  qtoprest  21741  ordthmeolem  21825  pt1hmeo  21830  xkocnv  21838  flimclslem  22008  flfval  22014  flfnei  22015  isflf  22017  flfcnp  22028  txflf  22030  supnfcls  22044  fclscf  22049  fclscmp  22054  fcfval  22057  isfcf  22058  uffcfflf  22063  cnpfcf  22065  mopnm  22469  isxms2  22473  prdsxmslem2  22554  bcth2  23346  dvmptid  23940  dvmptc  23941  dvtaylp  24344  taylthlem1  24347  taylthlem2  24348  pige3  24490  dvcxp1  24702  cxpcn3  24710  ordtrestNEW  30307  ordtrest2NEWlem  30308  ordtrest2NEW  30309  topjoin  32697  areacirclem1  33832