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∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
ntrnei.f ⊢F=𝒫BOB
ntrnei.r ⊢φ→IFN
Assertion ntrneicls11 ⊢φ→I⁡∅=∅↔∀x∈B¬∅∈N⁡x

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
2 ntrnei.f ⊢F=𝒫BOB
3 ntrnei.r ⊢φ→IFN
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 ffvelcdmd ⊢φ→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→IFN
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