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	⊢ ( 𝜑 → 𝐽 ∈ Top )
Assertion	opnneir	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		opnneir.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		anass	⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑥 ) ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) ) )
3		opnneiss	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
4	3	3expib	⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
5	4	anim1d	⊢ ( 𝐽 ∈ Top → ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑥 ) ∧ 𝜓 ) → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝜓 ) ) )
6	2 5	syl5bir	⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) ) → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝜓 ) ) )
7	6	reximdv2	⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 ) )
8	1 7	syl	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 ) )