Theorem toponmax 21677

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∪ cuni 4796  ‘cfv 6339  Topctop 21644  TopOnctopon 21661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-iota 6297  df-fun 6341  df-fv 6347  df-top 21645  df-topon 21662

This theorem is referenced by:  topgele  21681  eltpsg  21694  en2top  21736  resttopon  21912  ordtrest  21953  ordtrest2lem  21954  ordtrest2  21955  lmfval  21983  cnpfval  21985  iscn  21986  iscnp  21988  lmbrf  22011  cncls  22025  cnconst2  22034  cnrest2  22037  cndis  22042  cnindis  22043  cnpdis  22044  lmfss  22047  lmres  22051  lmff  22052  ist1-3  22100  connsuba  22171  unconn  22180  kgenval  22286  elkgen  22287  kgentopon  22289  pttoponconst  22348  tx1cn  22360  tx2cn  22361  ptcls  22367  xkoccn  22370  txlm  22399  cnmpt2res  22428  xkoinjcn  22438  qtoprest  22468  ordthmeolem  22552  pt1hmeo  22557  xkocnv  22565  flimclslem  22735  flfval  22741  flfnei  22742  isflf  22744  flfcnp  22755  txflf  22757  supnfcls  22771  fclscf  22776  fclscmp  22781  fcfval  22784  isfcf  22785  uffcfflf  22790  cnpfcf  22792  mopnm  23197  isxms2  23201  prdsxmslem2  23282  bcth2  24082  dvmptid  24709  dvmptc  24710  dvtaylp  25117  taylthlem1  25120  taylthlem2  25121  pige3ALT  25264  dvcxp1  25481  cxpcn3  25489  ordtrestNEW  31443  ordtrest2NEWlem  31444  ordtrest2NEW  31445  topjoin  34192  areacirclem1  35488