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 )