Theorem toponmax 22075

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 22063	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 22062	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2738	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 22055	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 17	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2839	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2106  ∪ cuni 4839  ‘cfv 6433  Topctop 22042  TopOnctopon 22059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-top 22043  df-topon 22060

This theorem is referenced by:  topgele  22079  eltpsg  22092  eltpsgOLD  22093  en2top  22135  resttopon  22312  ordtrest  22353  ordtrest2lem  22354  ordtrest2  22355  lmfval  22383  cnpfval  22385  iscn  22386  iscnp  22388  lmbrf  22411  cncls  22425  cnconst2  22434  cnrest2  22437  cndis  22442  cnindis  22443  cnpdis  22444  lmfss  22447  lmres  22451  lmff  22452  ist1-3  22500  connsuba  22571  unconn  22580  kgenval  22686  elkgen  22687  kgentopon  22689  pttoponconst  22748  tx1cn  22760  tx2cn  22761  ptcls  22767  xkoccn  22770  txlm  22799  cnmpt2res  22828  xkoinjcn  22838  qtoprest  22868  ordthmeolem  22952  pt1hmeo  22957  xkocnv  22965  flimclslem  23135  flfval  23141  flfnei  23142  isflf  23144  flfcnp  23155  txflf  23157  supnfcls  23171  fclscf  23176  fclscmp  23181  fcfval  23184  isfcf  23185  uffcfflf  23190  cnpfcf  23192  mopnm  23597  isxms2  23601  prdsxmslem2  23685  bcth2  24494  dvmptid  25121  dvmptc  25122  dvtaylp  25529  taylthlem1  25532  taylthlem2  25533  pige3ALT  25676  dvcxp1  25893  cxpcn3  25901  ordtrestNEW  31871  ordtrest2NEWlem  31872  ordtrest2NEW  31873  topjoin  34554  areacirclem1  35865