Theorem topopn 19393

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

Hypothesis

Ref	Expression
1open.1	|- X = U. J

Assertion

Ref	Expression
topopn	|- ( J e. Top -> X e. J )

Proof of Theorem topopn

Step	Hyp	Ref	Expression
1		1open.1	. 2 |- X = U. J
2		ssid 3508	. . 3 |- J C_ J
3		uniopn 19384	. . 3 |- ( ( J e. Top /\ J C_ J ) -> U. J e. J )
4	2, 3	mpan2 671	. 2 |- ( J e. Top -> U. J e. J )
5	1, 4	syl5eqel 2535	1 |- ( J e. Top -> X e. J )

Syntax hints:   -> wi 4   = wceq 1383   e. wcel 1804   C_ wss 3461   U.cuni 4234   Topctop 19372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-v 3097  df-in 3468  df-ss 3475  df-pw 3999  df-uni 4235  df-top 19377

This theorem is referenced by:  riinopn  19395  istps2OLD  19400  toponmax  19407  cldval  19502  ntrfval  19503  clsfval  19504  iscld  19506  ntrval  19515  clsval  19516  0cld  19517  clsval2  19529  ntrtop  19549  toponmre  19572  neifval  19578  neif  19579  neival  19581  isnei  19582  tpnei  19600  lpfval  19617  lpval  19618  restcld  19651  restcls  19660  restntr  19661  cnrest  19764  cmpsub  19878  hauscmplem  19884  cmpfi  19886  iscon2  19893  consubclo  19903  1stcfb  19924  1stcelcls  19940  islly2  19963  lly1stc  19975  islocfin  19996  finlocfin  19999  cmpkgen  20030  llycmpkgen  20031  ptbasid  20054  ptpjpre2  20059  ptopn2  20063  xkoopn  20068  xkouni  20078  txcld  20082  txcn  20105  ptrescn  20118  txtube  20119  txhaus  20126  xkoptsub  20133  xkopt  20134  xkopjcn  20135  qtoptop  20179  qtopuni  20181  opnfbas  20321  flimval  20442  flimfil  20448  hausflim  20460  hauspwpwf1  20466  hauspwpwdom  20467  flimfnfcls  20507  cnpfcfi  20519  bcthlem5  21745  dvply1  22658  cldssbrsiga  28136  dya2iocucvr  28233  kur14lem7  28634  kur14lem9  28636  conpcon  28658  cvmliftmolem1  28704  ordtop  29877  reopn  31430