Metamath Proof Explorer

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 ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
ntrnei.f ⊢ F = 𝒫 B O B
ntrnei.r ⊢ φ → I F N
Assertion ntrneineine1 ⊢ φ → ∀ x ∈ B ∃ s ∈ 𝒫 B ¬ x ∈ I ⁡ s ↔ ∀ x ∈ B N ⁡ x ≠ 𝒫 B

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
2 ntrnei.f ⊢ F = 𝒫 B O B
3 ntrnei.r ⊢ φ → I F N
4 3 adantr ⊢ φ ∧ x ∈ B → I F N
5 simpr ⊢ φ ∧ x ∈ B → x ∈ B
6 1 2 4 5 ntrneineine1lem ⊢ φ ∧ x ∈ B → ∃ s ∈ 𝒫 B ¬ x ∈ I ⁡ s ↔ N ⁡ x ≠ 𝒫 B
7 6 ralbidva ⊢ φ → ∀ x ∈ B ∃ s ∈ 𝒫 B ¬ x ∈ I ⁡ s ↔ ∀ x ∈ B N ⁡ x ≠ 𝒫 B