Metamath Proof Explorer

Theorem ntrclsk4

Description: Idempotence of the interior function is equivalent to idempotence of the closure function. (Contributed by RP, 10-Jul-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 ntrclsk4 
|- ( ph -> ( A. s e. ~P B ( I ` ( I ` s ) ) = ( I ` s ) <-> A. s e. ~P B ( K ` ( K ` s ) ) = ( 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 2fveq3 
 |-  ( s = t -> ( I ` ( I ` s ) ) = ( I ` ( I ` t ) ) )
5 fveq2 
 |-  ( s = t -> ( I ` s ) = ( I ` t ) )
6 4 5 eqeq12d 
 |-  ( s = t -> ( ( I ` ( I ` s ) ) = ( I ` s ) <-> ( I ` ( I ` t ) ) = ( I ` t ) ) )
7 6 cbvralvw 
 |-  ( A. s e. ~P B ( I ` ( I ` s ) ) = ( I ` s ) <-> A. t e. ~P B ( I ` ( I ` t ) ) = ( I ` 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 eqcomd 
 |-  ( t e. ~P B -> t = ( B \ ( B \ t ) ) )
19 18 adantl 
 |-  ( ( 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 2fveq3 
 |-  ( t = ( B \ s ) -> ( I ` ( I ` t ) ) = ( I ` ( I ` ( B \ s ) ) ) )
22 fveq2 
 |-  ( t = ( B \ s ) -> ( I ` t ) = ( I ` ( B \ s ) ) )
23 21 22 eqeq12d 
 |-  ( t = ( B \ s ) -> ( ( I ` ( I ` t ) ) = ( I ` t ) <-> ( I ` ( I ` ( B \ s ) ) ) = ( I ` ( B \ s ) ) ) )
24 23 3ad2ant3 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( ( I ` ( I ` t ) ) = ( I ` t ) <-> ( I ` ( I ` ( B \ s ) ) ) = ( I ` ( 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 8 ffvelrnd 
 |-  ( ph -> ( I ` ( B \ s ) ) e. ~P B )
29 27 28 ffvelrnd 
 |-  ( ph -> ( I ` ( I ` ( B \ s ) ) ) e. ~P B )
30 29 elpwid 
 |-  ( ph -> ( I ` ( I ` ( B \ s ) ) ) C_ B )
31 28 elpwid 
 |-  ( ph -> ( I ` ( B \ s ) ) C_ B )
32 rcompleq 
 |-  ( ( ( I ` ( I ` ( B \ s ) ) ) C_ B /\ ( I ` ( B \ s ) ) C_ B ) -> ( ( I ` ( I ` ( B \ s ) ) ) = ( I ` ( B \ s ) ) <-> ( B \ ( I ` ( I ` ( B \ s ) ) ) ) = ( B \ ( I ` ( B \ s ) ) ) ) )
33 30 31 32 syl2anc 
 |-  ( ph -> ( ( I ` ( I ` ( B \ s ) ) ) = ( I ` ( B \ s ) ) <-> ( B \ ( I ` ( I ` ( B \ s ) ) ) ) = ( B \ ( I ` ( B \ s ) ) ) ) )
34 33 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> ( ( I ` ( I ` ( B \ s ) ) ) = ( I ` ( B \ s ) ) <-> ( B \ ( I ` ( I ` ( B \ s ) ) ) ) = ( B \ ( I ` ( B \ s ) ) ) ) )
35 1 2 3 ntrclsnvobr 
 |-  ( ph -> K D I )
36 35 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> K D I )
37 1 2 35 ntrclsiex 
 |-  ( ph -> K e. ( ~P B ^m ~P B ) )
38 elmapi 
 |-  ( K e. ( ~P B ^m ~P B ) -> K : ~P B --> ~P B )
39 37 38 syl 
 |-  ( ph -> K : ~P B --> ~P B )
40 39 ffvelrnda 
 |-  ( ( ph /\ s e. ~P B ) -> ( K ` s ) e. ~P B )
41 1 2 36 40 ntrclsfv 
 |-  ( ( ph /\ s e. ~P B ) -> ( K ` ( K ` s ) ) = ( B \ ( I ` ( B \ ( K ` s ) ) ) ) )
42 simpr 
 |-  ( ( ph /\ s e. ~P B ) -> s e. ~P B )
43 1 2 36 42 ntrclsfv 
 |-  ( ( ph /\ s e. ~P B ) -> ( K ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
44 43 difeq2d 
 |-  ( ( ph /\ s e. ~P B ) -> ( B \ ( K ` s ) ) = ( B \ ( B \ ( I ` ( B \ s ) ) ) ) )
45 dfss4 
 |-  ( ( I ` ( B \ s ) ) C_ B <-> ( B \ ( B \ ( I ` ( B \ s ) ) ) ) = ( I ` ( B \ s ) ) )
46 31 45 sylib 
 |-  ( ph -> ( B \ ( B \ ( I ` ( B \ s ) ) ) ) = ( I ` ( B \ s ) ) )
47 46 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> ( B \ ( B \ ( I ` ( B \ s ) ) ) ) = ( I ` ( B \ s ) ) )
48 44 47 eqtrd 
 |-  ( ( ph /\ s e. ~P B ) -> ( B \ ( K ` s ) ) = ( I ` ( B \ s ) ) )
49 48 fveq2d 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` ( B \ ( K ` s ) ) ) = ( I ` ( I ` ( B \ s ) ) ) )
50 49 difeq2d 
 |-  ( ( ph /\ s e. ~P B ) -> ( B \ ( I ` ( B \ ( K ` s ) ) ) ) = ( B \ ( I ` ( I ` ( B \ s ) ) ) ) )
51 41 50 eqtrd 
 |-  ( ( ph /\ s e. ~P B ) -> ( K ` ( K ` s ) ) = ( B \ ( I ` ( I ` ( B \ s ) ) ) ) )
52 51 43 eqeq12d 
 |-  ( ( ph /\ s e. ~P B ) -> ( ( K ` ( K ` s ) ) = ( K ` s ) <-> ( B \ ( I ` ( I ` ( B \ s ) ) ) ) = ( B \ ( I ` ( B \ s ) ) ) ) )
53 34 52 bitr4d 
 |-  ( ( ph /\ s e. ~P B ) -> ( ( I ` ( I ` ( B \ s ) ) ) = ( I ` ( B \ s ) ) <-> ( K ` ( K ` s ) ) = ( K ` s ) ) )
54 53 3adant3 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( ( I ` ( I ` ( B \ s ) ) ) = ( I ` ( B \ s ) ) <-> ( K ` ( K ` s ) ) = ( K ` s ) ) )
55 24 54 bitrd 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( ( I ` ( I ` t ) ) = ( I ` t ) <-> ( K ` ( K ` s ) ) = ( K ` s ) ) )
56 9 20 55 ralxfrd2 
 |-  ( ph -> ( A. t e. ~P B ( I ` ( I ` t ) ) = ( I ` t ) <-> A. s e. ~P B ( K ` ( K ` s ) ) = ( K ` s ) ) )
57 7 56 syl5bb 
 |-  ( ph -> ( A. s e. ~P B ( I ` ( I ` s ) ) = ( I ` s ) <-> A. s e. ~P B ( K ` ( K ` s ) ) = ( K ` s ) ) )