Theorem topopn 22871

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 3944	. . 3 ⊢ 𝐽 ⊆ 𝐽
3		uniopn 22862	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽)
4	2, 3	mpan2 692	. 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
5	1, 4	eqeltrid 2840	1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ⊆ wss 3889  ∪ cuni 4850  Topctop 22858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906  df-pw 4543  df-uni 4851  df-top 22859

This theorem is referenced by:  riinopn  22873  toponmax  22891  cldval  22988  ntrfval  22989  clsfval  22990  iscld  22992  ntrval  23001  clsval  23002  0cld  23003  clsval2  23015  ntrtop  23035  toponmre  23058  neifval  23064  neif  23065  neival  23067  isnei  23068  tpnei  23086  lpfval  23103  lpval  23104  restcld  23137  restcls  23146  restntr  23147  cnrest  23250  cmpsub  23365  hauscmplem  23371  cmpfi  23373  isconn2  23379  connsubclo  23389  1stcfb  23410  1stcelcls  23426  islly2  23449  lly1stc  23461  islocfin  23482  finlocfin  23485  cmpkgen  23516  llycmpkgen  23517  ptbasid  23540  ptpjpre2  23545  ptopn2  23549  xkoopn  23554  xkouni  23564  txcld  23568  txcn  23591  ptrescn  23604  txtube  23605  txhaus  23612  xkoptsub  23619  xkopt  23620  xkopjcn  23621  qtoptop  23665  qtopuni  23667  opnfbas  23807  flimval  23928  flimfil  23934  hausflim  23946  hauspwpwf1  23952  hauspwpwdom  23953  flimfnfcls  23993  cnpfcfi  24005  bcthlem5  25295  dvply1  26250  cldssbrsiga  34331  dya2iocucvr  34428  kur14lem7  35394  kur14lem9  35396  connpconn  35417  cvmliftmolem1  35463  ordtop  36618  pibt2  37733  ntrelmap  44552  clselmap  44554  dssmapntrcls  44555  dssmapclsntr  44556  toprestsubel  45584  reopn  45722  toplatglb0  49474