This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ntridm

Description: The interior operation is idempotent. (Contributed by NM, 2-Oct-2007)

Ref Expression
Hypothesis clscld.1 ⊢ 𝑋 = ∪ 𝐽
Assertion ntridm ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

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