Theorem toponmax 22648

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 22636	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 22635	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2730	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 22628	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 17	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2831	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2104  ∪ cuni 4907  ‘cfv 6542  Topctop 22615  TopOnctopon 22632

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6494  df-fun 6544  df-fv 6550  df-top 22616  df-topon 22633

This theorem is referenced by:  topgele  22652  eltpsg  22665  eltpsgOLD  22666  en2top  22708  resttopon  22885  ordtrest  22926  ordtrest2lem  22927  ordtrest2  22928  lmfval  22956  cnpfval  22958  iscn  22959  iscnp  22961  lmbrf  22984  cncls  22998  cnconst2  23007  cnrest2  23010  cndis  23015  cnindis  23016  cnpdis  23017  lmfss  23020  lmres  23024  lmff  23025  ist1-3  23073  connsuba  23144  unconn  23153  kgenval  23259  elkgen  23260  kgentopon  23262  pttoponconst  23321  tx1cn  23333  tx2cn  23334  ptcls  23340  xkoccn  23343  txlm  23372  cnmpt2res  23401  xkoinjcn  23411  qtoprest  23441  ordthmeolem  23525  pt1hmeo  23530  xkocnv  23538  flimclslem  23708  flfval  23714  flfnei  23715  isflf  23717  flfcnp  23728  txflf  23730  supnfcls  23744  fclscf  23749  fclscmp  23754  fcfval  23757  isfcf  23758  uffcfflf  23763  cnpfcf  23765  mopnm  24170  isxms2  24174  prdsxmslem2  24258  bcth2  25078  dvmptid  25709  dvmptc  25710  dvtaylp  26118  taylthlem1  26121  taylthlem2  26122  pige3ALT  26265  dvcxp1  26484  cxpcn3  26492  ordtrestNEW  33199  ordtrest2NEWlem  33200  ordtrest2NEW  33201  topjoin  35553  areacirclem1  36879