Theorem topopn 21516

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 3991	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 21507	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 689	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2919	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114   ⊆ wss 3938  ∪ cuni 4840  Topctop 21503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rab 3149  df-v 3498  df-in 3945  df-ss 3954  df-pw 4543  df-uni 4841  df-top 21504

This theorem is referenced by:  riinopn  21518  toponmax  21536  cldval  21633  ntrfval  21634  clsfval  21635  iscld  21637  ntrval  21646  clsval  21647  0cld  21648  clsval2  21660  ntrtop  21680  toponmre  21703  neifval  21709  neif  21710  neival  21712  isnei  21713  tpnei  21731  lpfval  21748  lpval  21749  restcld  21782  restcls  21791  restntr  21792  cnrest  21895  cmpsub  22010  hauscmplem  22016  cmpfi  22018  isconn2  22024  connsubclo  22034  1stcfb  22055  1stcelcls  22071  islly2  22094  lly1stc  22106  islocfin  22127  finlocfin  22130  cmpkgen  22161  llycmpkgen  22162  ptbasid  22185  ptpjpre2  22190  ptopn2  22194  xkoopn  22199  xkouni  22209  txcld  22213  txcn  22236  ptrescn  22249  txtube  22250  txhaus  22257  xkoptsub  22264  xkopt  22265  xkopjcn  22266  qtoptop  22310  qtopuni  22312  opnfbas  22452  flimval  22573  flimfil  22579  hausflim  22591  hauspwpwf1  22597  hauspwpwdom  22598  flimfnfcls  22638  cnpfcfi  22650  bcthlem5  23933  dvply1  24875  cldssbrsiga  31448  dya2iocucvr  31544  kur14lem7  32461  kur14lem9  32463  connpconn  32484  cvmliftmolem1  32530  ordtop  33786  pibt2  34700  ntrelmap  40482  clselmap  40484  dssmapntrcls  40485  dssmapclsntr  40486  reopn  41562