This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ntrdif

Description: An interior of a complement is the complement of the closure. This set is also known as the exterior of A . (Contributed by Jeff Hankins, 31-Aug-2009)

		Ref	Expression
	Hypothesis	clscld.1	⊢ 𝑋 = ∪ 𝐽
	Assertion	ntrdif	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2		difss	⊢ ( 𝑋 ∖ 𝐴 ) ⊆ 𝑋
3	1	ntrval2	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝐴 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) )
4	2 3	mpan2	⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) )
5	4	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) )
6		simpr	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 )
7		dfss4	⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 )
8	6 7	sylib	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 )
9	8	fveq2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
10	9	difeq2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
11	5 10	eqtrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )