Metamath Proof Explorer

Theorem ntrneicls00

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that the closure of the empty set is the empty set hold equally. (Contributed by RP, 2-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 ntrneicls00 ⊢ φ → I ⁡ B = B ↔ ∀ x ∈ B 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 1 2 3 ntrneiiex ⊢ φ → I ∈ 𝒫 B 𝒫 B
5 elmapi ⊢ I ∈ 𝒫 B 𝒫 B → I : 𝒫 B ⟶ 𝒫 B
6 4 5 syl ⊢ φ → I : 𝒫 B ⟶ 𝒫 B
7 1 2 3 ntrneibex ⊢ φ → B ∈ V
8 pwidg ⊢ B ∈ V → B ∈ 𝒫 B
9 7 8 syl ⊢ φ → B ∈ 𝒫 B
10 6 9 ffvelcdmd ⊢ φ → I ⁡ B ∈ 𝒫 B
11 10 elpwid ⊢ φ → I ⁡ B ⊆ B
12 eqss ⊢ I ⁡ B = B ↔ I ⁡ B ⊆ B ∧ B ⊆ I ⁡ B
13 dfss3 ⊢ B ⊆ I ⁡ B ↔ ∀ x ∈ B x ∈ I ⁡ B
14 13 anbi2i ⊢ I ⁡ B ⊆ B ∧ B ⊆ I ⁡ B ↔ I ⁡ B ⊆ B ∧ ∀ x ∈ B x ∈ I ⁡ B
15 12 14 bitri ⊢ I ⁡ B = B ↔ I ⁡ B ⊆ B ∧ ∀ x ∈ B x ∈ I ⁡ B
16 15 a1i ⊢ φ → I ⁡ B = B ↔ I ⁡ B ⊆ B ∧ ∀ x ∈ B x ∈ I ⁡ B
17 11 16 mpbirand ⊢ φ → I ⁡ B = B ↔ ∀ x ∈ B x ∈ I ⁡ B
18 3 adantr ⊢ φ ∧ x ∈ B → I F N
19 simpr ⊢ φ ∧ x ∈ B → x ∈ B
20 9 adantr ⊢ φ ∧ x ∈ B → B ∈ 𝒫 B
21 1 2 18 19 20 ntrneiel ⊢ φ ∧ x ∈ B → x ∈ I ⁡ B ↔ B ∈ N ⁡ x
22 21 ralbidva ⊢ φ → ∀ x ∈ B x ∈ I ⁡ B ↔ ∀ x ∈ B B ∈ N ⁡ x
23 17 22 bitrd ⊢ φ → I ⁡ B = B ↔ ∀ x ∈ B B ∈ N ⁡ x