Theorem toponmax 23064

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∪ cuni 4873  ‘cfv 6538  Topctop 23031  TopOnctopon 23048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-top 23032  df-topon 23049

This theorem is referenced by:  topgele  23068  eltpsg  23081  en2top  23123  resttopon  23299  ordtrest  23340  ordtrest2lem  23341  ordtrest2  23342  lmfval  23370  cnpfval  23372  iscn  23373  iscnp  23375  lmbrf  23398  cncls  23412  cnconst2  23421  cnrest2  23424  cndis  23429  cnindis  23430  cnpdis  23431  lmfss  23434  lmres  23438  lmff  23439  ist1-3  23487  connsuba  23558  unconn  23567  kgenval  23673  elkgen  23674  kgentopon  23676  pttoponconst  23735  tx1cn  23747  tx2cn  23748  ptcls  23754  xkoccn  23757  txlm  23786  cnmpt2res  23815  xkoinjcn  23825  qtoprest  23855  ordthmeolem  23939  pt1hmeo  23944  xkocnv  23952  flimclslem  24122  flfval  24128  flfnei  24129  isflf  24131  flfcnp  24142  txflf  24144  supnfcls  24158  fclscf  24163  fclscmp  24168  fcfval  24171  isfcf  24172  uffcfflf  24177  cnpfcf  24179  mopnm  24582  isxms2  24586  prdsxmslem2  24667  bcth2  25470  dvmptid  26097  dvmptc  26098  dvtaylp  26511  taylthlem1  26514  taylthlem2  26515  pige3ALT  26663  dvcxp1  26883  cxpcn3  26891  ordtrestNEW  34289  ordtrest2NEWlem  34290  ordtrest2NEW  34291  topjoin  36854  areacirclem1  38337