Metamath Proof Explorer


Theorem ntrneix2

Description: An interior (closure) function is expansive if and only if all subsets which contain a point are neighborhoods (convergents) of that point. (Contributed by RP, 11-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 ntrneix2 φ s 𝒫 B s I s x B s 𝒫 B x s 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 simpr φ s 𝒫 B s 𝒫 B
5 elpwi s 𝒫 B s B
6 5 sselda s 𝒫 B x s x B
7 biimt x B x I s x B x I s
8 6 7 syl s 𝒫 B x s x I s x B x I s
9 8 pm5.74da s 𝒫 B x s x I s x s x B x I s
10 bi2.04 x s x B x I s x B x s x I s
11 9 10 bitrdi s 𝒫 B x s x I s x B x s x I s
12 11 albidv s 𝒫 B x x s x I s x x B x s x I s
13 dfss2 s I s x x s x I s
14 df-ral x B x s x I s x x B x s x I s
15 12 13 14 3bitr4g s 𝒫 B s I s x B x s x I s
16 4 15 syl φ s 𝒫 B s I s x B x s x I s
17 3 ad2antrr φ s 𝒫 B x B I F N
18 simpr φ s 𝒫 B x B x B
19 simplr φ s 𝒫 B x B s 𝒫 B
20 1 2 17 18 19 ntrneiel φ s 𝒫 B x B x I s s N x
21 20 imbi2d φ s 𝒫 B x B x s x I s x s s N x
22 21 ralbidva φ s 𝒫 B x B x s x I s x B x s s N x
23 16 22 bitrd φ s 𝒫 B s I s x B x s s N x
24 23 ralbidva φ s 𝒫 B s I s s 𝒫 B x B x s s N x
25 ralcom s 𝒫 B x B x s s N x x B s 𝒫 B x s s N x
26 24 25 bitrdi φ s 𝒫 B s I s x B s 𝒫 B x s s N x