Metamath Proof Explorer

Theorem ntrclsk2

Description: An interior function is contracting if and only if the closure function is expansive. (Contributed by RP, 9-Jun-2021)

Ref Expression
Hypotheses ntrcls.o 
|- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
ntrcls.d 
|- D = ( O ` B )
ntrcls.r 
|- ( ph -> I D K )
Assertion ntrclsk2 
|- ( ph -> ( A. s e. ~P B ( I ` s ) C_ s <-> A. s e. ~P B s C_ ( K ` s ) ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o 
 |-  O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
2 ntrcls.d 
 |-  D = ( O ` B )
3 ntrcls.r 
 |-  ( ph -> I D K )
4 fveq2 
 |-  ( s = t -> ( I ` s ) = ( I ` t ) )
5 id 
 |-  ( s = t -> s = t )
6 4 5 sseq12d 
 |-  ( s = t -> ( ( I ` s ) C_ s <-> ( I ` t ) C_ t ) )
7 6 cbvralvw 
 |-  ( A. s e. ~P B ( I ` s ) C_ s <-> A. t e. ~P B ( I ` t ) C_ t )
8 2 3 ntrclsrcomplex 
 |-  ( ph -> ( B \ s ) e. ~P B )
9 8 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> ( B \ s ) e. ~P B )
10 2 3 ntrclsrcomplex 
 |-  ( ph -> ( B \ t ) e. ~P B )
11 10 adantr 
 |-  ( ( ph /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
12 difeq2 
 |-  ( s = ( B \ t ) -> ( B \ s ) = ( B \ ( B \ t ) ) )
13 12 eqeq2d 
 |-  ( s = ( B \ t ) -> ( t = ( B \ s ) <-> t = ( B \ ( B \ t ) ) ) )
14 13 adantl 
 |-  ( ( ( ph /\ t e. ~P B ) /\ s = ( B \ t ) ) -> ( t = ( B \ s ) <-> t = ( B \ ( B \ t ) ) ) )
15 elpwi 
 |-  ( t e. ~P B -> t C_ B )
16 dfss4 
 |-  ( t C_ B <-> ( B \ ( B \ t ) ) = t )
17 15 16 sylib 
 |-  ( t e. ~P B -> ( B \ ( B \ t ) ) = t )
18 17 adantl 
 |-  ( ( ph /\ t e. ~P B ) -> ( B \ ( B \ t ) ) = t )
19 18 eqcomd 
 |-  ( ( ph /\ t e. ~P B ) -> t = ( B \ ( B \ t ) ) )
20 11 14 19 rspcedvd 
 |-  ( ( ph /\ t e. ~P B ) -> E. s e. ~P B t = ( B \ s ) )
21 fveq2 
 |-  ( t = ( B \ s ) -> ( I ` t ) = ( I ` ( B \ s ) ) )
22 id 
 |-  ( t = ( B \ s ) -> t = ( B \ s ) )
23 21 22 sseq12d 
 |-  ( t = ( B \ s ) -> ( ( I ` t ) C_ t <-> ( I ` ( B \ s ) ) C_ ( B \ s ) ) )
24 23 3ad2ant3 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( ( I ` t ) C_ t <-> ( I ` ( B \ s ) ) C_ ( B \ s ) ) )
25 1 2 3 ntrclsiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
26 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
27 25 26 syl 
 |-  ( ph -> I : ~P B --> ~P B )
28 27 3ad2ant1 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> I : ~P B --> ~P B )
29 8 3ad2ant1 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( B \ s ) e. ~P B )
30 28 29 ffvelcdmd 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( I ` ( B \ s ) ) e. ~P B )
31 30 elpwid 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( I ` ( B \ s ) ) C_ B )
32 difssd 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( B \ s ) C_ B )
33 sscon34b 
 |-  ( ( ( I ` ( B \ s ) ) C_ B /\ ( B \ s ) C_ B ) -> ( ( I ` ( B \ s ) ) C_ ( B \ s ) <-> ( B \ ( B \ s ) ) C_ ( B \ ( I ` ( B \ s ) ) ) ) )
34 31 32 33 syl2anc 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( ( I ` ( B \ s ) ) C_ ( B \ s ) <-> ( B \ ( B \ s ) ) C_ ( B \ ( I ` ( B \ s ) ) ) ) )
35 simp2 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> s e. ~P B )
36 elpwi 
 |-  ( s e. ~P B -> s C_ B )
37 dfss4 
 |-  ( s C_ B <-> ( B \ ( B \ s ) ) = s )
38 36 37 sylib 
 |-  ( s e. ~P B -> ( B \ ( B \ s ) ) = s )
39 38 sseq1d 
 |-  ( s e. ~P B -> ( ( B \ ( B \ s ) ) C_ ( B \ ( I ` ( B \ s ) ) ) <-> s C_ ( B \ ( I ` ( B \ s ) ) ) ) )
40 35 39 syl 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( ( B \ ( B \ s ) ) C_ ( B \ ( I ` ( B \ s ) ) ) <-> s C_ ( B \ ( I ` ( B \ s ) ) ) ) )
41 34 40 bitrd 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( ( I ` ( B \ s ) ) C_ ( B \ s ) <-> s C_ ( B \ ( I ` ( B \ s ) ) ) ) )
42 2 3 ntrclsbex 
 |-  ( ph -> B e. _V )
43 42 3ad2ant1 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> B e. _V )
44 25 3ad2ant1 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> I e. ( ~P B ^m ~P B ) )
45 eqid 
 |-  ( D ` I ) = ( D ` I )
46 eqid 
 |-  ( ( D ` I ) ` s ) = ( ( D ` I ) ` s )
47 1 2 43 44 45 35 46 dssmapfv3d 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( ( D ` I ) ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
48 47 sseq2d 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( s C_ ( ( D ` I ) ` s ) <-> s C_ ( B \ ( I ` ( B \ s ) ) ) ) )
49 1 2 3 ntrclsfv1 
 |-  ( ph -> ( D ` I ) = K )
50 49 fveq1d 
 |-  ( ph -> ( ( D ` I ) ` s ) = ( K ` s ) )
51 50 sseq2d 
 |-  ( ph -> ( s C_ ( ( D ` I ) ` s ) <-> s C_ ( K ` s ) ) )
52 51 3ad2ant1 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( s C_ ( ( D ` I ) ` s ) <-> s C_ ( K ` s ) ) )
53 41 48 52 3bitr2d 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( ( I ` ( B \ s ) ) C_ ( B \ s ) <-> s C_ ( K ` s ) ) )
54 24 53 bitrd 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( ( I ` t ) C_ t <-> s C_ ( K ` s ) ) )
55 9 20 54 ralxfrd2 
 |-  ( ph -> ( A. t e. ~P B ( I ` t ) C_ t <-> A. s e. ~P B s C_ ( K ` s ) ) )
56 7 55 bitrid 
 |-  ( ph -> ( A. s e. ~P B ( I ` s ) C_ s <-> A. s e. ~P B s C_ ( K ` s ) ) )