Metamath Proof Explorer

Theorem ntrneiel2

Description: Membership in iterated interior of a set is equivalent to there existing a particular neighborhood of that member such that points are members of that neighborhood if and only if the set is a neighborhood of each of those points. (Contributed by RP, 11-Jul-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 )
ntrneiel2.x 
|- ( ph -> X e. B )
ntrneiel2.s 
|- ( ph -> S e. ~P B )
Assertion ntrneiel2 
|- ( ph -> ( X e. ( I ` ( I ` S ) ) <-> E. u e. ( N ` X ) A. y e. B ( y e. u <-> S e. ( N ` y ) ) ) )

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 ntrneiel2.x 
 |-  ( ph -> X e. B )
5 ntrneiel2.s 
 |-  ( ph -> S e. ~P B )
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 5 ffvelrnd 
 |-  ( ph -> ( I ` S ) e. ~P B )
10 1 2 3 4 9 ntrneiel 
 |-  ( ph -> ( X e. ( I ` ( I ` S ) ) <-> ( I ` S ) e. ( N ` X ) ) )
11 1 2 3 5 ntrneifv4 
 |-  ( ph -> ( I ` S ) = { y e. B | S e. ( N ` y ) } )
12 df-rab 
 |-  { y e. B | S e. ( N ` y ) } = { y | ( y e. B /\ S e. ( N ` y ) ) }
13 11 12 eqtrdi 
 |-  ( ph -> ( I ` S ) = { y | ( y e. B /\ S e. ( N ` y ) ) } )
14 13 eleq1d 
 |-  ( ph -> ( ( I ` S ) e. ( N ` X ) <-> { y | ( y e. B /\ S e. ( N ` y ) ) } e. ( N ` X ) ) )
15 clabel 
 |-  ( { y | ( y e. B /\ S e. ( N ` y ) ) } e. ( N ` X ) <-> E. u ( u e. ( N ` X ) /\ A. y ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) ) )
16 df-rex 
 |-  ( E. u e. ( N ` X ) A. y ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) <-> E. u ( u e. ( N ` X ) /\ A. y ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) ) )
17 15 16 bitr4i 
 |-  ( { y | ( y e. B /\ S e. ( N ` y ) ) } e. ( N ` X ) <-> E. u e. ( N ` X ) A. y ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) )
18 ibar 
 |-  ( y e. B -> ( S e. ( N ` y ) <-> ( y e. B /\ S e. ( N ` y ) ) ) )
19 18 bibi2d 
 |-  ( y e. B -> ( ( y e. u <-> S e. ( N ` y ) ) <-> ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) ) )
20 19 ralbiia 
 |-  ( A. y e. B ( y e. u <-> S e. ( N ` y ) ) <-> A. y e. B ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) )
21 ssv 
 |-  B C_ _V
22 21 a1i 
 |-  ( ( ph /\ u e. ( N ` X ) ) -> B C_ _V )
23 vex 
 |-  y e. _V
24 eldif 
 |-  ( y e. ( _V \ B ) <-> ( y e. _V /\ -. y e. B ) )
25 23 24 mpbiran 
 |-  ( y e. ( _V \ B ) <-> -. y e. B )
26 1 2 3 ntrneinex 
 |-  ( ph -> N e. ( ~P ~P B ^m B ) )
27 elmapi 
 |-  ( N e. ( ~P ~P B ^m B ) -> N : B --> ~P ~P B )
28 26 27 syl 
 |-  ( ph -> N : B --> ~P ~P B )
29 28 4 ffvelrnd 
 |-  ( ph -> ( N ` X ) e. ~P ~P B )
30 29 elpwid 
 |-  ( ph -> ( N ` X ) C_ ~P B )
31 30 sselda 
 |-  ( ( ph /\ u e. ( N ` X ) ) -> u e. ~P B )
32 31 elpwid 
 |-  ( ( ph /\ u e. ( N ` X ) ) -> u C_ B )
33 32 sseld 
 |-  ( ( ph /\ u e. ( N ` X ) ) -> ( y e. u -> y e. B ) )
34 33 con3dimp 
 |-  ( ( ( ph /\ u e. ( N ` X ) ) /\ -. y e. B ) -> -. y e. u )
35 pm3.14 
 |-  ( ( -. y e. B \/ -. S e. ( N ` y ) ) -> -. ( y e. B /\ S e. ( N ` y ) ) )
36 35 orcs 
 |-  ( -. y e. B -> -. ( y e. B /\ S e. ( N ` y ) ) )
37 36 adantl 
 |-  ( ( ( ph /\ u e. ( N ` X ) ) /\ -. y e. B ) -> -. ( y e. B /\ S e. ( N ` y ) ) )
38 34 37 2falsed 
 |-  ( ( ( ph /\ u e. ( N ` X ) ) /\ -. y e. B ) -> ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) )
39 38 ex 
 |-  ( ( ph /\ u e. ( N ` X ) ) -> ( -. y e. B -> ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) ) )
40 25 39 syl5bi 
 |-  ( ( ph /\ u e. ( N ` X ) ) -> ( y e. ( _V \ B ) -> ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) ) )
41 40 ralrimiv 
 |-  ( ( ph /\ u e. ( N ` X ) ) -> A. y e. ( _V \ B ) ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) )
42 22 41 raldifeq 
 |-  ( ( ph /\ u e. ( N ` X ) ) -> ( A. y e. B ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) <-> A. y e. _V ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) ) )
43 20 42 syl5bb 
 |-  ( ( ph /\ u e. ( N ` X ) ) -> ( A. y e. B ( y e. u <-> S e. ( N ` y ) ) <-> A. y e. _V ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) ) )
44 ralv 
 |-  ( A. y e. _V ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) <-> A. y ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) )
45 43 44 bitr2di 
 |-  ( ( ph /\ u e. ( N ` X ) ) -> ( A. y ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) <-> A. y e. B ( y e. u <-> S e. ( N ` y ) ) ) )
46 45 rexbidva 
 |-  ( ph -> ( E. u e. ( N ` X ) A. y ( y e. u <-> ( y e. B /\ S e. ( N ` y ) ) ) <-> E. u e. ( N ` X ) A. y e. B ( y e. u <-> S e. ( N ` y ) ) ) )
47 17 46 syl5bb 
 |-  ( ph -> ( { y | ( y e. B /\ S e. ( N ` y ) ) } e. ( N ` X ) <-> E. u e. ( N ` X ) A. y e. B ( y e. u <-> S e. ( N ` y ) ) ) )
48 10 14 47 3bitrd 
 |-  ( ph -> ( X e. ( I ` ( I ` S ) ) <-> E. u e. ( N ` X ) A. y e. B ( y e. u <-> S e. ( N ` y ) ) ) )