Metamath Proof Explorer

Theorem topbnd

Description: Two equivalent expressions for the boundary of a topology. (Contributed by Jeff Hankins, 23-Sep-2009)

Ref Expression
Hypothesis topbnd.1 ⊢ X = ⋃ J
Assertion topbnd ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ A ∩ cls ⁡ J ⁡ X ∖ A = cls ⁡ J ⁡ A ∖ int ⁡ J ⁡ A

Proof

Step Hyp Ref Expression
1 topbnd.1 ⊢ X = ⋃ J
2 1 clsdif ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ X ∖ A = X ∖ int ⁡ J ⁡ A
3 2 ineq2d ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ A ∩ cls ⁡ J ⁡ X ∖ A = cls ⁡ J ⁡ A ∩ X ∖ int ⁡ J ⁡ A
4 indif2 ⊢ cls ⁡ J ⁡ A ∩ X ∖ int ⁡ J ⁡ A = cls ⁡ J ⁡ A ∩ X ∖ int ⁡ J ⁡ A
5 3 4 eqtrdi ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ A ∩ cls ⁡ J ⁡ X ∖ A = cls ⁡ J ⁡ A ∩ X ∖ int ⁡ J ⁡ A
6 1 clsss3 ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ A ⊆ X
7 df-ss ⊢ cls ⁡ J ⁡ A ⊆ X ↔ cls ⁡ J ⁡ A ∩ X = cls ⁡ J ⁡ A
8 6 7 sylib ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ A ∩ X = cls ⁡ J ⁡ A
9 8 difeq1d ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ A ∩ X ∖ int ⁡ J ⁡ A = cls ⁡ J ⁡ A ∖ int ⁡ J ⁡ A
10 5 9 eqtrd ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ A ∩ cls ⁡ J ⁡ X ∖ A = cls ⁡ J ⁡ A ∖ int ⁡ J ⁡ A