Theorem toponmax 23157

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 23145	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
2		topontop 23144	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
3		eqid 2762	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn 23137	. . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	2, 4	syl 18	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽)
6	1, 5	eqeltrd 2862	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∪ cuni 4870  ‘cfv 6537  Topctop 23124  TopOnctopon 23141

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-top 23125  df-topon 23142

This theorem is used by:  topgele  23161  eltpsg  23174  en2top  23216  resttopon  23392  ordtrest  23433  ordtrest2lem  23434  ordtrest2  23435  lmfval  23463  cnpfval  23465  iscn  23466  iscnp  23468  lmbrf  23491  cncls  23505  cnconst2  23514  cnrest2  23517  cndis  23522  cnindis  23523  cnpdis  23524  lmfss  23527  lmres  23531  lmff  23532  ist1-3  23580  connsuba  23651  unconn  23660  kgenval  23767  elkgen  23768  kgentopon  23770  pttoponconst  23829  tx1cn  23841  tx2cn  23842  ptcls  23848  xkoccn  23851  txlm  23880  cnmpt2res  23909  xkoinjcn  23919  qtoprest  23949  ordthmeolem  24033  pt1hmeo  24038  xkocnv  24046  flimclslem  24216  flfval  24222  flfnei  24223  isflf  24225  flfcnp  24236  txflf  24238  supnfcls  24252  fclscf  24257  fclscmp  24262  fcfval  24265  isfcf  24266  uffcfflf  24271  cnpfcf  24273  mopnm  24676  isxms2  24680  prdsxmslem2  24761  bcth2  25564  dvmptid  26191  dvmptc  26192  dvtaylp  26613  taylthlem1  26616  taylthlem2  26617  pige3ALT  26765  dvcxp1  26985  cxpcn3  26993  ordtrestNEW  34439  ordtrest2NEWlem  34440  ordtrest2NEW  34441  topjoin  36992  areacirclem1  38465