Theorem opnneir

Description: If something is true for an open neighborhood, it must be true for a neighborhood. (Contributed by Zhi Wang, 31-Aug-2024)

	Ref	Expression
Hypothesis	opnneir.1	|- ( ph -> J e. Top )
Assertion	opnneir	|- ( ph -> ( E. x e. J ( S C_ x /\ ps ) -> E. x e. ( ( nei ` J ) ` S ) ps ) )

Proof

Step	Hyp	Ref	Expression
1		opnneir.1	|- ( ph -> J e. Top )
2		anass	|- ( ( ( x e. J /\ S C_ x ) /\ ps ) <-> ( x e. J /\ ( S C_ x /\ ps ) ) )
3		opnneiss	|- ( ( J e. Top /\ x e. J /\ S C_ x ) -> x e. ( ( nei ` J ) ` S ) )
4	3	3expib	|- ( J e. Top -> ( ( x e. J /\ S C_ x ) -> x e. ( ( nei ` J ) ` S ) ) )
5	4	anim1d	|- ( J e. Top -> ( ( ( x e. J /\ S C_ x ) /\ ps ) -> ( x e. ( ( nei ` J ) ` S ) /\ ps ) ) )
6	2 5	syl5bir	|- ( J e. Top -> ( ( x e. J /\ ( S C_ x /\ ps ) ) -> ( x e. ( ( nei ` J ) ` S ) /\ ps ) ) )
7	6	reximdv2	|- ( J e. Top -> ( E. x e. J ( S C_ x /\ ps ) -> E. x e. ( ( nei ` J ) ` S ) ps ) )
8	1 7	syl	|- ( ph -> ( E. x e. J ( S C_ x /\ ps ) -> E. x e. ( ( nei ` J ) ` S ) ps ) )