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