Theorem topopn 14819

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 3248	. . 3 |- J C_ J
3		uniopn 14812	. . 3 |- ( ( J e. Top /\ J C_ J ) -> U. J e. J )
4	2, 3	mpan2 425	. 2 |- ( J e. Top -> U. J e. J )
5	1, 4	eqeltrid 2318	1 |- ( J e. Top -> X e. J )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2202   C_ wss 3201   U.cuni 3898   Topctop 14808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-in 3207  df-ss 3214  df-pw 3658  df-uni 3899  df-top 14809

This theorem is referenced by:  toponmax  14836  cldval  14910  ntrfval  14911  clsfval  14912  iscld  14914  ntrval  14921  clsval  14922  0cld  14923  ntrtop  14939  neifval  14951  neif  14952  neival  14954  isnei  14955  tpnei  14971  cnrest  15046  txcn  15086  dvply1  15576