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 = U. J
Assertion topbnd 
|- ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) = ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) )

Proof

Step Hyp Ref Expression
1 topbnd.1 
 |-  X = U. J
2 1 clsdif 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` ( X \ A ) ) = ( X \ ( ( int ` J ) ` A ) ) )
3 2 ineq2d 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) = ( ( ( cls ` J ) ` A ) i^i ( X \ ( ( int ` J ) ` A ) ) ) )
4 indif2 
 |-  ( ( ( cls ` J ) ` A ) i^i ( X \ ( ( int ` J ) ` A ) ) ) = ( ( ( ( cls ` J ) ` A ) i^i X ) \ ( ( int ` J ) ` A ) )
5 3 4 eqtrdi 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) = ( ( ( ( cls ` J ) ` A ) i^i X ) \ ( ( int ` J ) ` A ) ) )
6 1 clsss3 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` A ) C_ X )
7 df-ss 
 |-  ( ( ( cls ` J ) ` A ) C_ X <-> ( ( ( cls ` J ) ` A ) i^i X ) = ( ( cls ` J ) ` A ) )
8 6 7 sylib 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` A ) i^i X ) = ( ( cls ` J ) ` A ) )
9 8 difeq1d 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( ( cls ` J ) ` A ) i^i X ) \ ( ( int ` J ) ` A ) ) = ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) )
10 5 9 eqtrd 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) = ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) )