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		dfss2	⊢ ( ( ( 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 ‘ 𝐽 ) ‘ 𝐴 ) ) )