Theorem topopn 22928

Description: The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.)

Hypothesis

Ref	Expression
1open.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
topopn	⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Proof of Theorem topopn

Step	Hyp	Ref	Expression
1		1open.1	. 2 ⊢ 𝑋 = ∪ 𝐽
2		ssid 4018	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22919	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 691	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2843	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106   ⊆ wss 3963  ∪ cuni 4912  Topctop 22915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-in 3970  df-ss 3980  df-pw 4607  df-uni 4913  df-top 22916

This theorem is referenced by:  riinopn  22930  toponmax  22948  cldval  23047  ntrfval  23048  clsfval  23049  iscld  23051  ntrval  23060  clsval  23061  0cld  23062  clsval2  23074  ntrtop  23094  toponmre  23117  neifval  23123  neif  23124  neival  23126  isnei  23127  tpnei  23145  lpfval  23162  lpval  23163  restcld  23196  restcls  23205  restntr  23206  cnrest  23309  cmpsub  23424  hauscmplem  23430  cmpfi  23432  isconn2  23438  connsubclo  23448  1stcfb  23469  1stcelcls  23485  islly2  23508  lly1stc  23520  islocfin  23541  finlocfin  23544  cmpkgen  23575  llycmpkgen  23576  ptbasid  23599  ptpjpre2  23604  ptopn2  23608  xkoopn  23613  xkouni  23623  txcld  23627  txcn  23650  ptrescn  23663  txtube  23664  txhaus  23671  xkoptsub  23678  xkopt  23679  xkopjcn  23680  qtoptop  23724  qtopuni  23726  opnfbas  23866  flimval  23987  flimfil  23993  hausflim  24005  hauspwpwf1  24011  hauspwpwdom  24012  flimfnfcls  24052  cnpfcfi  24064  bcthlem5  25376  dvply1  26340  cldssbrsiga  34168  dya2iocucvr  34266  kur14lem7  35197  kur14lem9  35199  connpconn  35220  cvmliftmolem1  35266  ordtop  36419  pibt2  37400  ntrelmap  44115  clselmap  44117  dssmapntrcls  44118  dssmapclsntr  44119  toprestsubel  45097  reopn  45240  toplatglb0  48788