Theorem ntrtop

Description: The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006)

	Ref	Expression
Hypothesis	clscld.1	⊢ 𝑋 = ∪ 𝐽
Assertion	ntrtop	⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
3		ssid	⊢ 𝑋 ⊆ 𝑋
4	1	isopn3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑋 ) → ( 𝑋 ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ) )
5	3 4	mpan2	⊢ ( 𝐽 ∈ Top → ( 𝑋 ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ) )
6	2 5	mpbid	⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )