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

Metamath Proof Explorer

Theorem isneip

Description: The predicate "the class N is a neighborhood of point P ". (Contributed by NM, 26-Feb-2007)

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

Proof

Step Hyp Ref Expression
1 neifval.1 ⊢ 𝑋 = ∪ 𝐽
2 snssi ⊢ ( 𝑃 ∈ 𝑋 → { 𝑃 } ⊆ 𝑋 )
3 1 isnei ⊢ ( ( 𝐽 ∈ Top ∧ { 𝑃 } ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
4 2 3 sylan2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
5 snssg ⊢ ( 𝑃 ∈ 𝑋 → ( 𝑃 ∈ 𝑔 ↔ { 𝑃 } ⊆ 𝑔 ) )
6 5 anbi1d ⊢ ( 𝑃 ∈ 𝑋 → ( ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ↔ ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
7 6 rexbidv ⊢ ( 𝑃 ∈ 𝑋 → ( ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ↔ ∃ 𝑔 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
8 7 anbi2d ⊢ ( 𝑃 ∈ 𝑋 → ( ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
9 8 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
10 4 9 bitr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )