Metamath Proof Explorer

Theorem ntrneixb

Description: The interiors (closures) of sets that span the base set also span the base set if and only if the neighborhoods (convergents) of every point contain at least one of every pair of sets that span the base set. (Contributed by RP, 11-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 )
Assertion ntrneixb 
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( s u. t ) = B -> ( ( I ` s ) u. ( I ` t ) ) = B ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s u. t ) = B -> ( s e. ( N ` x ) \/ t 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 eqss 
 |-  ( ( ( I ` s ) u. ( I ` t ) ) = B <-> ( ( ( I ` s ) u. ( I ` t ) ) C_ B /\ B C_ ( ( I ` s ) u. ( I ` t ) ) ) )
5 4 a1i 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( I ` s ) u. ( I ` t ) ) = B <-> ( ( ( I ` s ) u. ( I ` t ) ) C_ B /\ B C_ ( ( I ` s ) u. ( I ` t ) ) ) ) )
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 ffvelcdmda 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` s ) e. ~P B )
10 9 elpwid 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` s ) C_ B )
11 10 adantr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` s ) C_ B )
12 8 ffvelcdmda 
 |-  ( ( ph /\ t e. ~P B ) -> ( I ` t ) e. ~P B )
13 12 elpwid 
 |-  ( ( ph /\ t e. ~P B ) -> ( I ` t ) C_ B )
14 13 adantlr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` t ) C_ B )
15 11 14 unssd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( I ` s ) u. ( I ` t ) ) C_ B )
16 15 biantrurd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( B C_ ( ( I ` s ) u. ( I ` t ) ) <-> ( ( ( I ` s ) u. ( I ` t ) ) C_ B /\ B C_ ( ( I ` s ) u. ( I ` t ) ) ) ) )
17 dfss3 
 |-  ( B C_ ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B x e. ( ( I ` s ) u. ( I ` t ) ) )
18 elun 
 |-  ( x e. ( ( I ` s ) u. ( I ` t ) ) <-> ( x e. ( I ` s ) \/ x e. ( I ` t ) ) )
19 18 ralbii 
 |-  ( A. x e. B x e. ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B ( x e. ( I ` s ) \/ x e. ( I ` t ) ) )
20 17 19 bitri 
 |-  ( B C_ ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B ( x e. ( I ` s ) \/ x e. ( I ` t ) ) )
21 20 a1i 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( B C_ ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B ( x e. ( I ` s ) \/ x e. ( I ` t ) ) ) )
22 5 16 21 3bitr2d 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( I ` s ) u. ( I ` t ) ) = B <-> A. x e. B ( x e. ( I ` s ) \/ x e. ( I ` t ) ) ) )
23 22 imbi2d 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( s u. t ) = B -> ( ( I ` s ) u. ( I ` t ) ) = B ) <-> ( ( s u. t ) = B -> A. x e. B ( x e. ( I ` s ) \/ x e. ( I ` t ) ) ) ) )
24 r19.21v 
 |-  ( A. x e. B ( ( s u. t ) = B -> ( x e. ( I ` s ) \/ x e. ( I ` t ) ) ) <-> ( ( s u. t ) = B -> A. x e. B ( x e. ( I ` s ) \/ x e. ( I ` t ) ) ) )
25 24 a1i 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. B ( ( s u. t ) = B -> ( x e. ( I ` s ) \/ x e. ( I ` t ) ) ) <-> ( ( s u. t ) = B -> A. x e. B ( x e. ( I ` s ) \/ x e. ( I ` t ) ) ) ) )
26 3 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> I F N )
27 simpr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> x e. B )
28 simpllr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> s e. ~P B )
29 1 2 26 27 28 ntrneiel 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` s ) <-> s e. ( N ` x ) ) )
30 simplr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> t e. ~P B )
31 1 2 26 27 30 ntrneiel 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` t ) <-> t e. ( N ` x ) ) )
32 29 31 orbi12d 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( x e. ( I ` s ) \/ x e. ( I ` t ) ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) )
33 32 imbi2d 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( ( s u. t ) = B -> ( x e. ( I ` s ) \/ x e. ( I ` t ) ) ) <-> ( ( s u. t ) = B -> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )
34 33 ralbidva 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. B ( ( s u. t ) = B -> ( x e. ( I ` s ) \/ x e. ( I ` t ) ) ) <-> A. x e. B ( ( s u. t ) = B -> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )
35 23 25 34 3bitr2d 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( s u. t ) = B -> ( ( I ` s ) u. ( I ` t ) ) = B ) <-> A. x e. B ( ( s u. t ) = B -> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )
36 35 ralbidva 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( ( s u. t ) = B -> ( ( I ` s ) u. ( I ` t ) ) = B ) <-> A. t e. ~P B A. x e. B ( ( s u. t ) = B -> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )
37 36 ralbidva 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( s u. t ) = B -> ( ( I ` s ) u. ( I ` t ) ) = B ) <-> A. s e. ~P B A. t e. ~P B A. x e. B ( ( s u. t ) = B -> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )
38 ralrot3 
 |-  ( A. s e. ~P B A. t e. ~P B A. x e. B ( ( s u. t ) = B -> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s u. t ) = B -> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) )
39 37 38 bitrdi 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( s u. t ) = B -> ( ( I ` s ) u. ( I ` t ) ) = B ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s u. t ) = B -> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )