Theorem toponmax 23224

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 23212	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 23211	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2761	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 23204	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 18	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2861	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∪ cuni 4867  ‘cfv 6531  Topctop 23191  TopOnctopon 23208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6487  df-fun 6533  df-fv 6539  df-top 23192  df-topon 23209

This theorem is used by:  topgele  23228  eltpsg  23241  en2top  23283  resttopon  23459  ordtrest  23500  ordtrest2lem  23501  ordtrest2  23502  lmfval  23530  cnpfval  23532  iscn  23533  iscnp  23535  lmbrf  23558  cncls  23572  cnconst2  23581  cnrest2  23584  cndis  23589  cnindis  23590  cnpdis  23591  lmfss  23594  lmres  23598  lmff  23599  ist1-3  23647  connsuba  23718  unconn  23727  kgenval  23834  elkgen  23835  kgentopon  23837  pttoponconst  23896  tx1cn  23908  tx2cn  23909  ptcls  23915  xkoccn  23918  txlm  23947  cnmpt2res  23976  xkoinjcn  23986  qtoprest  24016  ordthmeolem  24100  pt1hmeo  24105  xkocnv  24113  flimclslem  24283  flfval  24289  flfnei  24290  isflf  24292  flfcnp  24303  txflf  24305  supnfcls  24319  fclscf  24324  fclscmp  24329  fcfval  24332  isfcf  24333  uffcfflf  24338  cnpfcf  24340  mopnm  24743  isxms2  24747  prdsxmslem2  24828  bcth2  25631  dvmptid  26257  dvmptc  26258  dvtaylp  26679  taylthlem1  26682  taylthlem2  26683  pige3ALT  26830  dvcxp1  27050  cxpcn3  27058  ordtrestNEW  34535  ordtrest2NEWlem  34536  ordtrest2NEW  34537  topjoin  37123  areacirclem1  38594