Metamath Proof Explorer


Theorem ntrneik2

Description: An interior function is contracting if and only if all the neighborhoods of a point contain 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 ntrneik2 φ s 𝒫 B I s s x B s 𝒫 B s N x x s

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 6 ffvelrnda φ s 𝒫 B I s 𝒫 B
8 7 elpwid φ s 𝒫 B I s B
9 8 sselda φ s 𝒫 B x I s x B
10 biimt x B x s x B x s
11 9 10 syl φ s 𝒫 B x I s x s x B x s
12 11 pm5.74da φ s 𝒫 B x I s x s x I s x B x s
13 bi2.04 x I s x B x s x B x I s x s
14 12 13 bitrdi φ s 𝒫 B x I s x s x B x I s x s
15 14 albidv φ s 𝒫 B x x I s x s x x B x I s x s
16 dfss2 I s s x x I s x s
17 df-ral x B x I s x s x x B x I s x s
18 15 16 17 3bitr4g φ s 𝒫 B I s s x B x I s x s
19 3 ad2antrr φ s 𝒫 B x B I F N
20 simpr φ s 𝒫 B x B x B
21 simplr φ s 𝒫 B x B s 𝒫 B
22 1 2 19 20 21 ntrneiel φ s 𝒫 B x B x I s s N x
23 22 imbi1d φ s 𝒫 B x B x I s x s s N x x s
24 23 ralbidva φ s 𝒫 B x B x I s x s x B s N x x s
25 18 24 bitrd φ s 𝒫 B I s s x B s N x x s
26 25 ralbidva φ s 𝒫 B I s s s 𝒫 B x B s N x x s
27 ralcom s 𝒫 B x B s N x x s x B s 𝒫 B s N x x s
28 26 27 bitrdi φ s 𝒫 B I s s x B s 𝒫 B s N x x s