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 ‘ 𝐽 ) ‘ 𝑆 ) )