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