Metamath Proof Explorer

Theorem ntrneineine0lem

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
ntrnei.x ⊢ φ → X ∈ B
Assertion ntrneineine0lem ⊢ φ → ∃ s ∈ 𝒫 B X ∈ I ⁡ s ↔ 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 ntrnei.x ⊢ φ → X ∈ B
5 3 adantr ⊢ φ ∧ s ∈ 𝒫 B → I F N
6 4 adantr ⊢ φ ∧ s ∈ 𝒫 B → X ∈ B
7 simpr ⊢ φ ∧ s ∈ 𝒫 B → s ∈ 𝒫 B
8 1 2 5 6 7 ntrneiel ⊢ φ ∧ s ∈ 𝒫 B → X ∈ I ⁡ s ↔ s ∈ N ⁡ X
9 8 rexbidva ⊢ φ → ∃ s ∈ 𝒫 B X ∈ I ⁡ s ↔ ∃ s ∈ 𝒫 B s ∈ N ⁡ X
10 1 2 3 ntrneinex ⊢ φ → N ∈ 𝒫 𝒫 B B
11 elmapi ⊢ N ∈ 𝒫 𝒫 B B → N : B ⟶ 𝒫 𝒫 B
12 10 11 syl ⊢ φ → N : B ⟶ 𝒫 𝒫 B
13 12 4 ffvelcdmd ⊢ φ → N ⁡ X ∈ 𝒫 𝒫 B
14 13 elpwid ⊢ φ → N ⁡ X ⊆ 𝒫 B
15 14 sseld ⊢ φ → s ∈ N ⁡ X → s ∈ 𝒫 B
16 15 pm4.71rd ⊢ φ → s ∈ N ⁡ X ↔ s ∈ 𝒫 B ∧ s ∈ N ⁡ X
17 16 exbidv ⊢ φ → ∃ s s ∈ N ⁡ X ↔ ∃ s s ∈ 𝒫 B ∧ s ∈ N ⁡ X
18 17 bicomd ⊢ φ → ∃ s s ∈ 𝒫 B ∧ s ∈ N ⁡ X ↔ ∃ s s ∈ N ⁡ X
19 df-rex ⊢ ∃ s ∈ 𝒫 B s ∈ N ⁡ X ↔ ∃ s s ∈ 𝒫 B ∧ s ∈ N ⁡ X
20 n0 ⊢ N ⁡ X ≠ ∅ ↔ ∃ s s ∈ N ⁡ X
21 18 19 20 3bitr4g ⊢ φ → ∃ s ∈ 𝒫 B s ∈ N ⁡ X ↔ N ⁡ X ≠ ∅
22 9 21 bitrd ⊢ φ → ∃ s ∈ 𝒫 B X ∈ I ⁡ s ↔ N ⁡ X ≠ ∅