Metamath Proof Explorer

Theorem ntrneineine1lem

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
ntrnei.x ⊢ φ → X ∈ B
Assertion ntrneineine1lem ⊢ φ → ∃ s ∈ 𝒫 B ¬ X ∈ I ⁡ s ↔ 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 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 notbid ⊢ φ ∧ s ∈ 𝒫 B → ¬ X ∈ I ⁡ s ↔ ¬ s ∈ N ⁡ X
10 9 rexbidva ⊢ φ → ∃ s ∈ 𝒫 B ¬ X ∈ I ⁡ s ↔ ∃ s ∈ 𝒫 B ¬ s ∈ N ⁡ X
11 1 2 3 ntrneinex ⊢ φ → N ∈ 𝒫 𝒫 B B
12 elmapi ⊢ N ∈ 𝒫 𝒫 B B → N : B ⟶ 𝒫 𝒫 B
13 11 12 syl ⊢ φ → N : B ⟶ 𝒫 𝒫 B
14 13 4 ffvelcdmd ⊢ φ → N ⁡ X ∈ 𝒫 𝒫 B
15 14 elpwid ⊢ φ → N ⁡ X ⊆ 𝒫 B
16 biortn ⊢ N ⁡ X ⊆ 𝒫 B → ¬ 𝒫 B ⊆ N ⁡ X ↔ ¬ N ⁡ X ⊆ 𝒫 B ∨ ¬ 𝒫 B ⊆ N ⁡ X
17 15 16 syl ⊢ φ → ¬ 𝒫 B ⊆ N ⁡ X ↔ ¬ N ⁡ X ⊆ 𝒫 B ∨ ¬ 𝒫 B ⊆ N ⁡ X
18 df-rex ⊢ ∃ s ∈ 𝒫 B ¬ s ∈ N ⁡ X ↔ ∃ s s ∈ 𝒫 B ∧ ¬ s ∈ N ⁡ X
19 nss ⊢ ¬ 𝒫 B ⊆ N ⁡ X ↔ ∃ s s ∈ 𝒫 B ∧ ¬ s ∈ N ⁡ X
20 18 19 bitr4i ⊢ ∃ s ∈ 𝒫 B ¬ s ∈ N ⁡ X ↔ ¬ 𝒫 B ⊆ N ⁡ X
21 df-ne ⊢ N ⁡ X ≠ 𝒫 B ↔ ¬ N ⁡ X = 𝒫 B
22 ianor ⊢ ¬ N ⁡ X ⊆ 𝒫 B ∧ 𝒫 B ⊆ N ⁡ X ↔ ¬ N ⁡ X ⊆ 𝒫 B ∨ ¬ 𝒫 B ⊆ N ⁡ X
23 eqss ⊢ N ⁡ X = 𝒫 B ↔ N ⁡ X ⊆ 𝒫 B ∧ 𝒫 B ⊆ N ⁡ X
24 22 23 xchnxbir ⊢ ¬ N ⁡ X = 𝒫 B ↔ ¬ N ⁡ X ⊆ 𝒫 B ∨ ¬ 𝒫 B ⊆ N ⁡ X
25 21 24 bitri ⊢ N ⁡ X ≠ 𝒫 B ↔ ¬ N ⁡ X ⊆ 𝒫 B ∨ ¬ 𝒫 B ⊆ N ⁡ X
26 17 20 25 3bitr4g ⊢ φ → ∃ s ∈ 𝒫 B ¬ s ∈ N ⁡ X ↔ N ⁡ X ≠ 𝒫 B
27 10 26 bitrd ⊢ φ → ∃ s ∈ 𝒫 B ¬ X ∈ I ⁡ s ↔ N ⁡ X ≠ 𝒫 B