Metamath Proof Explorer

Theorem ntrneicls11

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that the interior of the empty set is the empty set hold equally. (Contributed by RP, 2-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 ntrneicls11 
|- ( ph -> ( ( I ` (/) ) = (/) <-> A. x e. B -. (/) 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 1 2 3 ntrneiiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
5 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
6 4 5 syl 
 |-  ( ph -> I : ~P B --> ~P B )
7 0elpw 
 |-  (/) e. ~P B
8 7 a1i 
 |-  ( ph -> (/) e. ~P B )
9 6 8 ffvelrnd 
 |-  ( ph -> ( I ` (/) ) e. ~P B )
10 9 elpwid 
 |-  ( ph -> ( I ` (/) ) C_ B )
11 reldisj 
 |-  ( ( I ` (/) ) C_ B -> ( ( ( I ` (/) ) i^i B ) = (/) <-> ( I ` (/) ) C_ ( B \ B ) ) )
12 10 11 syl 
 |-  ( ph -> ( ( ( I ` (/) ) i^i B ) = (/) <-> ( I ` (/) ) C_ ( B \ B ) ) )
13 12 bicomd 
 |-  ( ph -> ( ( I ` (/) ) C_ ( B \ B ) <-> ( ( I ` (/) ) i^i B ) = (/) ) )
14 difid 
 |-  ( B \ B ) = (/)
15 14 sseq2i 
 |-  ( ( I ` (/) ) C_ ( B \ B ) <-> ( I ` (/) ) C_ (/) )
16 ss0b 
 |-  ( ( I ` (/) ) C_ (/) <-> ( I ` (/) ) = (/) )
17 15 16 bitri 
 |-  ( ( I ` (/) ) C_ ( B \ B ) <-> ( I ` (/) ) = (/) )
18 disjr 
 |-  ( ( ( I ` (/) ) i^i B ) = (/) <-> A. x e. B -. x e. ( I ` (/) ) )
19 13 17 18 3bitr3g 
 |-  ( ph -> ( ( I ` (/) ) = (/) <-> A. x e. B -. x e. ( I ` (/) ) ) )
20 3 adantr 
 |-  ( ( ph /\ x e. B ) -> I F N )
21 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
22 7 a1i 
 |-  ( ( ph /\ x e. B ) -> (/) e. ~P B )
23 1 2 20 21 22 ntrneiel 
 |-  ( ( ph /\ x e. B ) -> ( x e. ( I ` (/) ) <-> (/) e. ( N ` x ) ) )
24 23 notbid 
 |-  ( ( ph /\ x e. B ) -> ( -. x e. ( I ` (/) ) <-> -. (/) e. ( N ` x ) ) )
25 24 ralbidva 
 |-  ( ph -> ( A. x e. B -. x e. ( I ` (/) ) <-> A. x e. B -. (/) e. ( N ` x ) ) )
26 19 25 bitrd 
 |-  ( ph -> ( ( I ` (/) ) = (/) <-> A. x e. B -. (/) e. ( N ` x ) ) )