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 𝑋 = 𝐽
Assertion topopn ( 𝐽 ∈ Top → 𝑋𝐽 )

Proof

Step Hyp Ref Expression
1 1open.1 𝑋 = 𝐽
2 ssid 𝐽𝐽
3 uniopn ( ( 𝐽 ∈ Top ∧ 𝐽𝐽 ) → 𝐽𝐽 )
4 2 3 mpan2 ( 𝐽 ∈ Top → 𝐽𝐽 )
5 1 4 eqeltrid ( 𝐽 ∈ Top → 𝑋𝐽 )