Metamath Proof Explorer

Theorem ntrneiiso

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that the interior function is isotonic hold equally. (Contributed by RP, 3-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 ntrneiiso 
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> 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 df-ss 
 |-  ( ( I ` s ) C_ ( I ` t ) <-> A. x ( x e. ( I ` s ) -> x e. ( I ` t ) ) )
5 4 imbi2i 
 |-  ( ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> ( s C_ t -> A. x ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) )
6 19.21v 
 |-  ( A. x ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> ( s C_ t -> A. x ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) )
7 5 6 bitr4i 
 |-  ( ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. x ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) )
8 ax-1 
 |-  ( ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) -> ( x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) )
9 simpll 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ph )
10 1 2 3 ntrneiiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
11 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
12 9 10 11 3syl 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> I : ~P B --> ~P B )
13 simplr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> s e. ~P B )
14 12 13 ffvelcdmd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` s ) e. ~P B )
15 14 elpwid 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` s ) C_ B )
16 15 sselda 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. ( I ` s ) ) -> x e. B )
17 16 pm2.24d 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. ( I ` s ) ) -> ( -. x e. B -> x e. ( I ` t ) ) )
18 17 ex 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( x e. ( I ` s ) -> ( -. x e. B -> x e. ( I ` t ) ) ) )
19 18 com23 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( -. x e. B -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) )
20 19 a1dd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( -. x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) )
21 idd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) )
22 20 21 jad 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) )
23 8 22 impbid2 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> ( x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) ) )
24 23 albidv 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> A. x ( x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) ) )
25 df-ral 
 |-  ( A. x e. B ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> A. x ( x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) )
26 24 25 bitr4di 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> A. x e. B ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) )
27 3 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> I F N )
28 simpr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> x e. B )
29 simpllr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> s e. ~P B )
30 1 2 27 28 29 ntrneiel 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` s ) <-> s e. ( N ` x ) ) )
31 simplr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> t e. ~P B )
32 1 2 27 28 31 ntrneiel 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` t ) <-> t e. ( N ` x ) ) )
33 30 32 imbi12d 
 |-  ( ( ( ( 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 ) ) ) )
34 33 imbi2d 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> ( s C_ t -> ( s e. ( N ` x ) -> t e. ( N ` x ) ) ) ) )
35 impexp 
 |-  ( ( ( s C_ t /\ s e. ( N ` x ) ) -> t e. ( N ` x ) ) <-> ( s C_ t -> ( s e. ( N ` x ) -> t e. ( N ` x ) ) ) )
36 ancomst 
 |-  ( ( ( s C_ t /\ s e. ( N ` x ) ) -> t e. ( N ` x ) ) <-> ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) )
37 35 36 bitr3i 
 |-  ( ( s C_ t -> ( s e. ( N ` x ) -> t e. ( N ` x ) ) ) <-> ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) )
38 34 37 bitrdi 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) )
39 38 ralbidva 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. B ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) )
40 26 39 bitrd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) )
41 7 40 bitrid 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) )
42 41 ralbidva 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. t e. ~P B A. x e. B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) )
43 ralcom 
 |-  ( A. t e. ~P B A. x e. B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) <-> A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) )
44 42 43 bitrdi 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) )
45 44 ralbidva 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. s e. ~P B A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) )
46 ralcom 
 |-  ( A. s e. ~P B A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) )
47 45 46 bitrdi 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) )