Metamath Proof Explorer

Theorem ntrclsiso

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that either is isotonic hold equally. (Contributed by RP, 3-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 ntrclsiso 
|- ( 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. t e. ~P B ( s C_ t -> ( K ` s ) C_ ( K ` t ) ) ) )

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 sseq1 
 |-  ( s = b -> ( s C_ t <-> b C_ t ) )
5 fveq2 
 |-  ( s = b -> ( I ` s ) = ( I ` b ) )
6 5 sseq1d 
 |-  ( s = b -> ( ( I ` s ) C_ ( I ` t ) <-> ( I ` b ) C_ ( I ` t ) ) )
7 4 6 imbi12d 
 |-  ( s = b -> ( ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> ( b C_ t -> ( I ` b ) C_ ( I ` t ) ) ) )
8 sseq2 
 |-  ( t = a -> ( b C_ t <-> b C_ a ) )
9 fveq2 
 |-  ( t = a -> ( I ` t ) = ( I ` a ) )
10 9 sseq2d 
 |-  ( t = a -> ( ( I ` b ) C_ ( I ` t ) <-> ( I ` b ) C_ ( I ` a ) ) )
11 8 10 imbi12d 
 |-  ( t = a -> ( ( b C_ t -> ( I ` b ) C_ ( I ` t ) ) <-> ( b C_ a -> ( I ` b ) C_ ( I ` a ) ) ) )
12 7 11 cbvral2vw 
 |-  ( A. s e. ~P B A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. b e. ~P B A. a e. ~P B ( b C_ a -> ( I ` b ) C_ ( I ` a ) ) )
13 ralcom 
 |-  ( A. b e. ~P B A. a e. ~P B ( b C_ a -> ( I ` b ) C_ ( I ` a ) ) <-> A. a e. ~P B A. b e. ~P B ( b C_ a -> ( I ` b ) C_ ( I ` a ) ) )
14 12 13 bitri 
 |-  ( A. s e. ~P B A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. a e. ~P B A. b e. ~P B ( b C_ a -> ( I ` b ) C_ ( I ` a ) ) )
15 simpl 
 |-  ( ( ph /\ s e. ~P B ) -> ph )
16 2 3 ntrclsbex 
 |-  ( ph -> B e. _V )
17 15 16 syl 
 |-  ( ( ph /\ s e. ~P B ) -> B e. _V )
18 difssd 
 |-  ( ( ph /\ s e. ~P B ) -> ( B \ s ) C_ B )
19 17 18 sselpwd 
 |-  ( ( ph /\ s e. ~P B ) -> ( B \ s ) e. ~P B )
20 elpwi 
 |-  ( a e. ~P B -> a C_ B )
21 simpl 
 |-  ( ( B e. _V /\ a C_ B ) -> B e. _V )
22 difssd 
 |-  ( ( B e. _V /\ a C_ B ) -> ( B \ a ) C_ B )
23 21 22 sselpwd 
 |-  ( ( B e. _V /\ a C_ B ) -> ( B \ a ) e. ~P B )
24 simpr 
 |-  ( ( ( B e. _V /\ a C_ B ) /\ s = ( B \ a ) ) -> s = ( B \ a ) )
25 24 difeq2d 
 |-  ( ( ( B e. _V /\ a C_ B ) /\ s = ( B \ a ) ) -> ( B \ s ) = ( B \ ( B \ a ) ) )
26 25 eqeq2d 
 |-  ( ( ( B e. _V /\ a C_ B ) /\ s = ( B \ a ) ) -> ( a = ( B \ s ) <-> a = ( B \ ( B \ a ) ) ) )
27 eqcom 
 |-  ( a = ( B \ ( B \ a ) ) <-> ( B \ ( B \ a ) ) = a )
28 26 27 bitrdi 
 |-  ( ( ( B e. _V /\ a C_ B ) /\ s = ( B \ a ) ) -> ( a = ( B \ s ) <-> ( B \ ( B \ a ) ) = a ) )
29 dfss4 
 |-  ( a C_ B <-> ( B \ ( B \ a ) ) = a )
30 29 bilani 
 |-  ( ( B e. _V /\ a C_ B ) -> ( B \ ( B \ a ) ) = a )
31 23 28 30 rspcedvd 
 |-  ( ( B e. _V /\ a C_ B ) -> E. s e. ~P B a = ( B \ s ) )
32 16 20 31 syl2an 
 |-  ( ( ph /\ a e. ~P B ) -> E. s e. ~P B a = ( B \ s ) )
33 simpl1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ph )
34 33 16 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> B e. _V )
35 difssd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ( B \ t ) C_ B )
36 34 35 sselpwd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
37 elpwi 
 |-  ( b e. ~P B -> b C_ B )
38 simpl 
 |-  ( ( B e. _V /\ b C_ B ) -> B e. _V )
39 difssd 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ b ) C_ B )
40 38 39 sselpwd 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ b ) e. ~P B )
41 simpr 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> t = ( B \ b ) )
42 41 difeq2d 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( B \ t ) = ( B \ ( B \ b ) ) )
43 42 eqeq2d 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( b = ( B \ t ) <-> b = ( B \ ( B \ b ) ) ) )
44 eqcom 
 |-  ( b = ( B \ ( B \ b ) ) <-> ( B \ ( B \ b ) ) = b )
45 43 44 bitrdi 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( b = ( B \ t ) <-> ( B \ ( B \ b ) ) = b ) )
46 dfss4 
 |-  ( b C_ B <-> ( B \ ( B \ b ) ) = b )
47 46 bilani 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ ( B \ b ) ) = b )
48 40 45 47 rspcedvd 
 |-  ( ( B e. _V /\ b C_ B ) -> E. t e. ~P B b = ( B \ t ) )
49 16 37 48 syl2an 
 |-  ( ( ph /\ b e. ~P B ) -> E. t e. ~P B b = ( B \ t ) )
50 49 3ad2antl1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ b e. ~P B ) -> E. t e. ~P B b = ( B \ t ) )
51 simp12 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> s e. ~P B )
52 51 elpwid 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> s C_ B )
53 simp2 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> t e. ~P B )
54 53 elpwid 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> t C_ B )
55 sscon34b 
 |-  ( ( s C_ B /\ t C_ B ) -> ( s C_ t <-> ( B \ t ) C_ ( B \ s ) ) )
56 52 54 55 syl2anc 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( s C_ t <-> ( B \ t ) C_ ( B \ s ) ) )
57 56 bicomd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( B \ t ) C_ ( B \ s ) <-> s C_ t ) )
58 simp11 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ph )
59 1 2 3 ntrclsiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
60 58 59 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> I e. ( ~P B ^m ~P B ) )
61 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
62 60 61 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> I : ~P B --> ~P B )
63 58 16 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> B e. _V )
64 difssd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( B \ t ) C_ B )
65 63 64 sselpwd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( B \ t ) e. ~P B )
66 62 65 ffvelcdmd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` ( B \ t ) ) e. ~P B )
67 66 elpwid 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` ( B \ t ) ) C_ B )
68 difssd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( B \ s ) C_ B )
69 63 68 sselpwd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( B \ s ) e. ~P B )
70 62 69 ffvelcdmd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` ( B \ s ) ) e. ~P B )
71 70 elpwid 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` ( B \ s ) ) C_ B )
72 sscon34b 
 |-  ( ( ( I ` ( B \ t ) ) C_ B /\ ( I ` ( B \ s ) ) C_ B ) -> ( ( I ` ( B \ t ) ) C_ ( I ` ( B \ s ) ) <-> ( B \ ( I ` ( B \ s ) ) ) C_ ( B \ ( I ` ( B \ t ) ) ) ) )
73 67 71 72 syl2anc 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( I ` ( B \ t ) ) C_ ( I ` ( B \ s ) ) <-> ( B \ ( I ` ( B \ s ) ) ) C_ ( B \ ( I ` ( B \ t ) ) ) ) )
74 57 73 imbi12d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( ( B \ t ) C_ ( B \ s ) -> ( I ` ( B \ t ) ) C_ ( I ` ( B \ s ) ) ) <-> ( s C_ t -> ( B \ ( I ` ( B \ s ) ) ) C_ ( B \ ( I ` ( B \ t ) ) ) ) ) )
75 simp3 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> b = ( B \ t ) )
76 simp13 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> a = ( B \ s ) )
77 75 76 sseq12d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( b C_ a <-> ( B \ t ) C_ ( B \ s ) ) )
78 75 fveq2d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` b ) = ( I ` ( B \ t ) ) )
79 76 fveq2d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` a ) = ( I ` ( B \ s ) ) )
80 78 79 sseq12d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( I ` b ) C_ ( I ` a ) <-> ( I ` ( B \ t ) ) C_ ( I ` ( B \ s ) ) ) )
81 77 80 imbi12d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( b C_ a -> ( I ` b ) C_ ( I ` a ) ) <-> ( ( B \ t ) C_ ( B \ s ) -> ( I ` ( B \ t ) ) C_ ( I ` ( B \ s ) ) ) ) )
82 1 2 3 ntrclsfv1 
 |-  ( ph -> ( D ` I ) = K )
83 58 82 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( D ` I ) = K )
84 83 fveq1d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( D ` I ) ` s ) = ( K ` s ) )
85 eqid 
 |-  ( D ` I ) = ( D ` I )
86 eqid 
 |-  ( ( D ` I ) ` s ) = ( ( D ` I ) ` s )
87 1 2 63 60 85 51 86 dssmapfv3d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( D ` I ) ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
88 84 87 eqtr3d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( K ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
89 58 3 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> I D K )
90 1 2 89 ntrclsfv1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( D ` I ) = K )
91 90 fveq1d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( D ` I ) ` t ) = ( K ` t ) )
92 eqid 
 |-  ( ( D ` I ) ` t ) = ( ( D ` I ) ` t )
93 1 2 63 60 85 53 92 dssmapfv3d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( D ` I ) ` t ) = ( B \ ( I ` ( B \ t ) ) ) )
94 91 93 eqtr3d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( K ` t ) = ( B \ ( I ` ( B \ t ) ) ) )
95 88 94 sseq12d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( K ` s ) C_ ( K ` t ) <-> ( B \ ( I ` ( B \ s ) ) ) C_ ( B \ ( I ` ( B \ t ) ) ) ) )
96 95 imbi2d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( s C_ t -> ( K ` s ) C_ ( K ` t ) ) <-> ( s C_ t -> ( B \ ( I ` ( B \ s ) ) ) C_ ( B \ ( I ` ( B \ t ) ) ) ) ) )
97 74 81 96 3bitr4d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( b C_ a -> ( I ` b ) C_ ( I ` a ) ) <-> ( s C_ t -> ( K ` s ) C_ ( K ` t ) ) ) )
98 36 50 97 ralxfrd2 
 |-  ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) -> ( A. b e. ~P B ( b C_ a -> ( I ` b ) C_ ( I ` a ) ) <-> A. t e. ~P B ( s C_ t -> ( K ` s ) C_ ( K ` t ) ) ) )
99 19 32 98 ralxfrd2 
 |-  ( ph -> ( A. a e. ~P B A. b e. ~P B ( b C_ a -> ( I ` b ) C_ ( I ` a ) ) <-> A. s e. ~P B A. t e. ~P B ( s C_ t -> ( K ` s ) C_ ( K ` t ) ) ) )
100 14 99 bitrid 
 |-  ( 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. t e. ~P B ( s C_ t -> ( K ` s ) C_ ( K ` t ) ) ) )