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 = J
Assertion topopn J Top X J


Step Hyp Ref Expression
1 1open.1 X = J
2 ssid J J
3 uniopn J Top J J J J
4 2 3 mpan2 J Top J J
5 1 4 eqeltrid J Top X J