Theorem isnei

Description: The predicate "the class N is a neighborhood of S ". (Contributed by FL, 25-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Hypothesis	neifval.1	⊢ 𝑋 = ∪ 𝐽
Assertion	isnei	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		neifval.1	⊢ 𝑋 = ∪ 𝐽
2	1	neival	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) = { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } )
3	2	eleq2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑁 ∈ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ) )
4		sseq2	⊢ ( 𝑣 = 𝑁 → ( 𝑔 ⊆ 𝑣 ↔ 𝑔 ⊆ 𝑁 ) )
5	4	anbi2d	⊢ ( 𝑣 = 𝑁 → ( ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) ↔ ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
6	5	rexbidv	⊢ ( 𝑣 = 𝑁 → ( ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) ↔ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
7	6	elrab	⊢ ( 𝑁 ∈ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ↔ ( 𝑁 ∈ 𝒫 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
8	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
9		elpw2g	⊢ ( 𝑋 ∈ 𝐽 → ( 𝑁 ∈ 𝒫 𝑋 ↔ 𝑁 ⊆ 𝑋 ) )
10	8 9	syl	⊢ ( 𝐽 ∈ Top → ( 𝑁 ∈ 𝒫 𝑋 ↔ 𝑁 ⊆ 𝑋 ) )
11	10	anbi1d	⊢ ( 𝐽 ∈ Top → ( ( 𝑁 ∈ 𝒫 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
12	7 11	syl5bb	⊢ ( 𝐽 ∈ Top → ( 𝑁 ∈ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
13	12	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
14	3 13	bitrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )