Theorem toponmax 23274

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 23262	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 23261	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2763	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 23254	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 18	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2864	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∪ cuni 4870  ‘cfv 6558  Topctop 23241  TopOnctopon 23258

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6512  df-fun 6560  df-fv 6566  df-top 23242  df-topon 23259

This theorem is used by:  topgele  23278  eltpsg  23291  en2top  23333  resttopon  23509  ordtrest  23550  ordtrest2lem  23551  ordtrest2  23552  lmfval  23580  cnpfval  23582  iscn  23583  iscnp  23585  lmbrf  23608  cncls  23622  cnconst2  23631  cnrest2  23634  cndis  23639  cnindis  23640  cnpdis  23641  lmfss  23644  lmres  23648  lmff  23649  ist1-3  23697  connsuba  23768  unconn  23777  kgenval  23884  elkgen  23885  kgentopon  23887  pttoponconst  23946  tx1cn  23958  tx2cn  23959  ptcls  23965  xkoccn  23968  txlm  23997  cnmpt2res  24026  xkoinjcn  24036  qtoprest  24066  ordthmeolem  24150  pt1hmeo  24155  xkocnv  24163  flimclslem  24333  flfval  24339  flfnei  24340  isflf  24342  flfcnp  24353  txflf  24355  supnfcls  24369  fclscf  24374  fclscmp  24379  fcfval  24382  isfcf  24383  uffcfflf  24388  cnpfcf  24390  mopnm  24793  isxms2  24797  prdsxmslem2  24878  bcth2  25681  dvmptid  26307  dvmptc  26308  dvtaylp  26727  taylthlem1  26730  taylthlem2  26731  pige3ALT  26878  dvcxp1  27098  cxpcn3  27106  ordtrestNEW  34623  ordtrest2NEWlem  34624  ordtrest2NEW  34625  topjoin  37331  areacirclem1  38818