Theorem toponmax 22966

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 22954	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 22953	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2761	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 22946	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 17	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2861	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2141  ∪ cuni 4864  ‘cfv 6517  Topctop 22933  TopOnctopon 22950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-iota 6473  df-fun 6519  df-fv 6525  df-top 22934  df-topon 22951

This theorem is referenced by:  topgele  22970  eltpsg  22983  en2top  23025  resttopon  23201  ordtrest  23242  ordtrest2lem  23243  ordtrest2  23244  lmfval  23272  cnpfval  23274  iscn  23275  iscnp  23277  lmbrf  23300  cncls  23314  cnconst2  23323  cnrest2  23326  cndis  23331  cnindis  23332  cnpdis  23333  lmfss  23336  lmres  23340  lmff  23341  ist1-3  23389  connsuba  23460  unconn  23469  kgenval  23575  elkgen  23576  kgentopon  23578  pttoponconst  23637  tx1cn  23649  tx2cn  23650  ptcls  23656  xkoccn  23659  txlm  23688  cnmpt2res  23717  xkoinjcn  23727  qtoprest  23757  ordthmeolem  23841  pt1hmeo  23846  xkocnv  23854  flimclslem  24024  flfval  24030  flfnei  24031  isflf  24033  flfcnp  24044  txflf  24046  supnfcls  24060  fclscf  24065  fclscmp  24070  fcfval  24073  isfcf  24074  uffcfflf  24079  cnpfcf  24081  mopnm  24484  isxms2  24488  prdsxmslem2  24569  bcth2  25372  dvmptid  25999  dvmptc  26000  dvtaylp  26410  taylthlem1  26413  taylthlem2  26414  pige3ALT  26562  dvcxp1  26782  cxpcn3  26790  ordtrestNEW  34179  ordtrest2NEWlem  34180  ordtrest2NEW  34181  topjoin  36689  areacirclem1  38171