Metamath Proof Explorer


Theorem topopn

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

Ref Expression
Hypothesis 1open.1
|- X = U. J
Assertion topopn
|- ( J e. Top -> X e. J )

Proof

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