Theorem ntrneineine1

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that for every point, at not all subsets are (pseudo-)neighborboods hold equally. (Contributed by RP, 1-Jun-2021)

	Ref	Expression
Hypotheses	ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
Assertion	ntrneineine1	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑁 ‘ 𝑥 ) ≠ 𝒫 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
6	1 2 4 5	ntrneineine1lem	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ( 𝑁 ‘ 𝑥 ) ≠ 𝒫 𝐵 ) )
7	6	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑁 ‘ 𝑥 ) ≠ 𝒫 𝐵 ) )