Theorem ntrval

Description: The interior of a subset of a topology's base set is the union of all the open sets it includes. Definition of interior of Munkres p. 94. (Contributed by NM, 10-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Hypothesis	iscld.1	⊢ 𝑋 = ∪ 𝐽
Assertion	ntrval	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		iscld.1	⊢ 𝑋 = ∪ 𝐽
2	1	ntrfval	⊢ ( 𝐽 ∈ Top → ( int ‘ 𝐽 ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) ) )
3	2	fveq1d	⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ( ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) ) ‘ 𝑆 ) )
4	3	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ( ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) ) ‘ 𝑆 ) )
5		eqid	⊢ ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) )
6		pweq	⊢ ( 𝑥 = 𝑆 → 𝒫 𝑥 = 𝒫 𝑆 )
7	6	ineq2d	⊢ ( 𝑥 = 𝑆 → ( 𝐽 ∩ 𝒫 𝑥 ) = ( 𝐽 ∩ 𝒫 𝑆 ) )
8	7	unieqd	⊢ ( 𝑥 = 𝑆 → ∪ ( 𝐽 ∩ 𝒫 𝑥 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
9	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
10		elpw2g	⊢ ( 𝑋 ∈ 𝐽 → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
11	9 10	syl	⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
12	11	biimpar	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ 𝒫 𝑋 )
13		inex1g	⊢ ( 𝐽 ∈ Top → ( 𝐽 ∩ 𝒫 𝑆 ) ∈ V )
14	13	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐽 ∩ 𝒫 𝑆 ) ∈ V )
15	14	uniexd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ∈ V )
16	5 8 12 15	fvmptd3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
17	4 16	eqtrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )