Metamath Proof Explorer

Theorem ntridm

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

Ref Expression
Hypothesis clscld.1 ⊢X=⋃J
Assertion ntridm ⊢J∈Top∧S⊆X→int⁡J⁡int⁡J⁡S=int⁡J⁡S

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢X=⋃J
2 1 ntropn ⊢J∈Top∧S⊆X→int⁡J⁡S∈J
3 1 ntrss3 ⊢J∈Top∧S⊆X→int⁡J⁡S⊆X
4 1 isopn3 ⊢J∈Top∧int⁡J⁡S⊆X→int⁡J⁡S∈J↔int⁡J⁡int⁡J⁡S=int⁡J⁡S
5 3 4 syldan ⊢J∈Top∧S⊆X→int⁡J⁡S∈J↔int⁡J⁡int⁡J⁡S=int⁡J⁡S
6 2 5 mpbid ⊢J∈Top∧S⊆X→int⁡J⁡int⁡J⁡S=int⁡J⁡S