Metamath Proof Explorer


Theorem ntrneifv4

Description: The value of the interior (closure) expressed in terms of the neighbors (convergents) function. (Contributed by RP, 26-Jun-2021)

Ref Expression
Hypotheses ntrnei.o
|- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
ntrnei.f
|- F = ( ~P B O B )
ntrnei.r
|- ( ph -> I F N )
ntrneifv.s
|- ( ph -> S e. ~P B )
Assertion ntrneifv4
|- ( ph -> ( I ` S ) = { x e. B | S e. ( N ` x ) } )

Proof

Step Hyp Ref Expression
1 ntrnei.o
 |-  O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
2 ntrnei.f
 |-  F = ( ~P B O B )
3 ntrnei.r
 |-  ( ph -> I F N )
4 ntrneifv.s
 |-  ( ph -> S e. ~P B )
5 dfin5
 |-  ( B i^i ( I ` S ) ) = { x e. B | x e. ( I ` S ) }
6 1 2 3 ntrneiiex
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
7 elmapi
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
8 6 7 syl
 |-  ( ph -> I : ~P B --> ~P B )
9 8 4 ffvelrnd
 |-  ( ph -> ( I ` S ) e. ~P B )
10 9 elpwid
 |-  ( ph -> ( I ` S ) C_ B )
11 sseqin2
 |-  ( ( I ` S ) C_ B <-> ( B i^i ( I ` S ) ) = ( I ` S ) )
12 10 11 sylib
 |-  ( ph -> ( B i^i ( I ` S ) ) = ( I ` S ) )
13 3 adantr
 |-  ( ( ph /\ x e. B ) -> I F N )
14 simpr
 |-  ( ( ph /\ x e. B ) -> x e. B )
15 4 adantr
 |-  ( ( ph /\ x e. B ) -> S e. ~P B )
16 1 2 13 14 15 ntrneiel
 |-  ( ( ph /\ x e. B ) -> ( x e. ( I ` S ) <-> S e. ( N ` x ) ) )
17 16 rabbidva
 |-  ( ph -> { x e. B | x e. ( I ` S ) } = { x e. B | S e. ( N ` x ) } )
18 5 12 17 3eqtr3a
 |-  ( ph -> ( I ` S ) = { x e. B | S e. ( N ` x ) } )