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 ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁𝑋 ∧ ∃ 𝑔𝐽 ( 𝑃𝑔𝑔𝑁 ) ) ) )