Theorem toponmax 22813

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∪ cuni 4871  ‘cfv 6511  Topctop 22780  TopOnctopon 22797

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-top 22781  df-topon 22798

This theorem is referenced by:  topgele  22817  eltpsg  22830  en2top  22872  resttopon  23048  ordtrest  23089  ordtrest2lem  23090  ordtrest2  23091  lmfval  23119  cnpfval  23121  iscn  23122  iscnp  23124  lmbrf  23147  cncls  23161  cnconst2  23170  cnrest2  23173  cndis  23178  cnindis  23179  cnpdis  23180  lmfss  23183  lmres  23187  lmff  23188  ist1-3  23236  connsuba  23307  unconn  23316  kgenval  23422  elkgen  23423  kgentopon  23425  pttoponconst  23484  tx1cn  23496  tx2cn  23497  ptcls  23503  xkoccn  23506  txlm  23535  cnmpt2res  23564  xkoinjcn  23574  qtoprest  23604  ordthmeolem  23688  pt1hmeo  23693  xkocnv  23701  flimclslem  23871  flfval  23877  flfnei  23878  isflf  23880  flfcnp  23891  txflf  23893  supnfcls  23907  fclscf  23912  fclscmp  23917  fcfval  23920  isfcf  23921  uffcfflf  23926  cnpfcf  23928  mopnm  24332  isxms2  24336  prdsxmslem2  24417  bcth2  25230  dvmptid  25861  dvmptc  25862  dvtaylp  26278  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  pige3ALT  26429  dvcxp1  26649  cxpcn3  26658  ordtrestNEW  33911  ordtrest2NEWlem  33912  ordtrest2NEW  33913  topjoin  36353  areacirclem1  37702