Theorem ntrval2

Description: Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2		difss	⊢ ( 𝑋 ∖ 𝑆 ) ⊆ 𝑋
3	1	clsval2	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝑆 ) ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝑆 ) ) ) ) )
4	2 3	mpan2	⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝑆 ) ) ) ) )
5	4	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝑆 ) ) ) ) )
6		dfss4	⊢ ( 𝑆 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝑆 ) ) = 𝑆 )
7	6	biimpi	⊢ ( 𝑆 ⊆ 𝑋 → ( 𝑋 ∖ ( 𝑋 ∖ 𝑆 ) ) = 𝑆 )
8	7	fveq2d	⊢ ( 𝑆 ⊆ 𝑋 → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝑆 ) ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
9	8	adantl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝑆 ) ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
10	9	difeq2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝑆 ) ) ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) )
11	5 10	eqtrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) )
12	11	difeq2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) = ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
13	1	ntropn	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 )
14	1	eltopss	⊢ ( ( 𝐽 ∈ Top ∧ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
15	13 14	syldan	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
16		dfss4	⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
17	15 16	sylib	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
18	12 17	eqtr2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) )