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

Metamath Proof Explorer

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 bitrid ⊢ ( 𝐽 ∈ Top → ( 𝑁 ∈ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
13 12 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
14 3 13 bitrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )