Metamath Proof Explorer

Theorem ntrneicls11

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that the interior 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 ntrneicls11 ⊢ φ → I ⁡ ∅ = ∅ ↔ ∀ 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 1 2 3 ntrneiiex ⊢ φ → I ∈ 𝒫 B 𝒫 B
5 elmapi ⊢ I ∈ 𝒫 B 𝒫 B → I : 𝒫 B ⟶ 𝒫 B
6 4 5 syl ⊢ φ → I : 𝒫 B ⟶ 𝒫 B
7 0elpw ⊢ ∅ ∈ 𝒫 B
8 7 a1i ⊢ φ → ∅ ∈ 𝒫 B
9 6 8 ffvelrnd ⊢ φ → I ⁡ ∅ ∈ 𝒫 B
10 9 elpwid ⊢ φ → I ⁡ ∅ ⊆ B
11 reldisj ⊢ I ⁡ ∅ ⊆ B → I ⁡ ∅ ∩ B = ∅ ↔ I ⁡ ∅ ⊆ B ∖ B
12 10 11 syl ⊢ φ → I ⁡ ∅ ∩ B = ∅ ↔ I ⁡ ∅ ⊆ B ∖ B
13 12 bicomd ⊢ φ → I ⁡ ∅ ⊆ B ∖ B ↔ I ⁡ ∅ ∩ B = ∅
14 difid ⊢ B ∖ B = ∅
15 14 sseq2i ⊢ I ⁡ ∅ ⊆ B ∖ B ↔ I ⁡ ∅ ⊆ ∅
16 ss0b ⊢ I ⁡ ∅ ⊆ ∅ ↔ I ⁡ ∅ = ∅
17 15 16 bitri ⊢ I ⁡ ∅ ⊆ B ∖ B ↔ I ⁡ ∅ = ∅
18 disjr ⊢ I ⁡ ∅ ∩ B = ∅ ↔ ∀ x ∈ B ¬ x ∈ I ⁡ ∅
19 13 17 18 3bitr3g ⊢ φ → I ⁡ ∅ = ∅ ↔ ∀ x ∈ B ¬ x ∈ I ⁡ ∅
20 3 adantr ⊢ φ ∧ x ∈ B → I F N
21 simpr ⊢ φ ∧ x ∈ B → x ∈ B
22 7 a1i ⊢ φ ∧ x ∈ B → ∅ ∈ 𝒫 B
23 1 2 20 21 22 ntrneiel ⊢ φ ∧ x ∈ B → x ∈ I ⁡ ∅ ↔ ∅ ∈ N ⁡ x
24 23 notbid ⊢ φ ∧ x ∈ B → ¬ x ∈ I ⁡ ∅ ↔ ¬ ∅ ∈ N ⁡ x
25 24 ralbidva ⊢ φ → ∀ x ∈ B ¬ x ∈ I ⁡ ∅ ↔ ∀ x ∈ B ¬ ∅ ∈ N ⁡ x
26 19 25 bitrd ⊢ φ → I ⁡ ∅ = ∅ ↔ ∀ x ∈ B ¬ ∅ ∈ N ⁡ x