Theorem neival

Description: Value of the set of neighborhoods of a subset of the base set of a topology. (Contributed by NM, 11-Feb-2007) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Hypothesis	neifval.1	⊢ 𝑋 = ∪ 𝐽
Assertion	neival	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) = { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } )

Proof

Step	Hyp	Ref	Expression
1		neifval.1	⊢ 𝑋 = ∪ 𝐽
2	1	neifval	⊢ ( 𝐽 ∈ Top → ( nei ‘ 𝐽 ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ) )
3	2	fveq1d	⊢ ( 𝐽 ∈ Top → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) = ( ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ) ‘ 𝑆 ) )
4	3	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) = ( ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ) ‘ 𝑆 ) )
5		eqid	⊢ ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } )
6		cleq1lem	⊢ ( 𝑥 = 𝑆 → ( ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) ↔ ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) ) )
7	6	rexbidv	⊢ ( 𝑥 = 𝑆 → ( ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) ↔ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) ) )
8	7	rabbidv	⊢ ( 𝑥 = 𝑆 → { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } = { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } )
9	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
10		elpw2g	⊢ ( 𝑋 ∈ 𝐽 → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
11	9 10	syl	⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
12	11	biimpar	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ 𝒫 𝑋 )
13		pwexg	⊢ ( 𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V )
14		rabexg	⊢ ( 𝒫 𝑋 ∈ V → { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ∈ V )
15	9 13 14	3syl	⊢ ( 𝐽 ∈ Top → { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ∈ V )
16	15	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ∈ V )
17	5 8 12 16	fvmptd3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ) ‘ 𝑆 ) = { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } )
18	4 17	eqtrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) = { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } )