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 𝑋 = 𝐽
Assertion topbnd ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋𝐴 ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 topbnd.1 𝑋 = 𝐽
2 1 clsdif ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋𝐴 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
3 2 ineq2d ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋𝐴 ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) )
4 indif2 ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ 𝑋 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
5 3 4 eqtrdi ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋𝐴 ) ) ) = ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ 𝑋 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
6 1 clsss3 ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 )
7 df-ss ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ 𝑋 ) = ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
8 6 7 sylib ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ 𝑋 ) = ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
9 8 difeq1d ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ 𝑋 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
10 5 9 eqtrd ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋𝐴 ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )