Metamath Proof Explorer

Theorem ntrneineine0

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that for every point, at least one (pseudo-)neighborbood exists hold equally. (Contributed by RP, 29-May-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 ntrneineine0 ⊢ φ → ∀ x ∈ B ∃ s ∈ 𝒫 B x ∈ I ⁡ s ↔ ∀ x ∈ B N ⁡ x ≠ ∅

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 ntrneineine0lem ⊢ φ ∧ x ∈ B → ∃ s ∈ 𝒫 B x ∈ I ⁡ s ↔ N ⁡ x ≠ ∅
7 6 ralbidva ⊢ φ → ∀ x ∈ B ∃ s ∈ 𝒫 B x ∈ I ⁡ s ↔ ∀ x ∈ B N ⁡ x ≠ ∅