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 biimpi 
 |-  ( a C_ B -> ( B \ ( B \ a ) ) = a )
31 30 adantl 
 |-  ( ( B e. _V /\ a C_ B ) -> ( B \ ( B \ a ) ) = a )
32 23 28 31 rspcedvd 
 |-  ( ( B e. _V /\ a C_ B ) -> E. s e. ~P B a = ( B \ s ) )
33 16 20 32 syl2an 
 |-  ( ( ph /\ a e. ~P B ) -> E. s e. ~P B a = ( B \ s ) )
34 simpl1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ph )
35 34 16 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> B e. _V )
36 difssd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ( B \ t ) C_ B )
37 35 36 sselpwd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
38 elpwi 
 |-  ( b e. ~P B -> b C_ B )
39 simpl 
 |-  ( ( B e. _V /\ b C_ B ) -> B e. _V )
40 difssd 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ b ) C_ B )
41 39 40 sselpwd 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ b ) e. ~P B )
42 simpr 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> t = ( B \ b ) )
43 42 difeq2d 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( B \ t ) = ( B \ ( B \ b ) ) )
44 43 eqeq2d 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( b = ( B \ t ) <-> b = ( B \ ( B \ b ) ) ) )
45 eqcom 
 |-  ( b = ( B \ ( B \ b ) ) <-> ( B \ ( B \ b ) ) = b )
46 44 45 bitrdi 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( b = ( B \ t ) <-> ( B \ ( B \ b ) ) = b ) )
47 dfss4 
 |-  ( b C_ B <-> ( B \ ( B \ b ) ) = b )
48 47 biimpi 
 |-  ( b C_ B -> ( B \ ( B \ b ) ) = b )
49 48 adantl 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ ( B \ b ) ) = b )
50 41 46 49 rspcedvd 
 |-  ( ( B e. _V /\ b C_ B ) -> E. t e. ~P B b = ( B \ t ) )
51 16 38 50 syl2an 
 |-  ( ( ph /\ b e. ~P B ) -> E. t e. ~P B b = ( B \ t ) )
52 51 3ad2antl1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ b e. ~P B ) -> E. t e. ~P B b = ( B \ t ) )
53 simp12 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> s e. ~P B )
54 53 elpwid 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> s C_ B )
55 simp2 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> t e. ~P B )
56 55 elpwid 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> t C_ B )
57 sscon34b 
 |-  ( ( s C_ B /\ t C_ B ) -> ( s C_ t <-> ( B \ t ) C_ ( B \ s ) ) )
58 54 56 57 syl2anc 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( s C_ t <-> ( B \ t ) C_ ( B \ s ) ) )
59 58 bicomd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( B \ t ) C_ ( B \ s ) <-> s C_ t ) )
60 simp11 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ph )
61 1 2 3 ntrclsiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
62 60 61 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> I e. ( ~P B ^m ~P B ) )
63 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
64 62 63 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> I : ~P B --> ~P B )
65 60 16 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> B e. _V )
66 difssd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( B \ t ) C_ B )
67 65 66 sselpwd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( B \ t ) e. ~P B )
68 64 67 ffvelrnd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` ( B \ t ) ) e. ~P B )
69 68 elpwid 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` ( B \ t ) ) C_ B )
70 difssd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( B \ s ) C_ B )
71 65 70 sselpwd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( B \ s ) e. ~P B )
72 64 71 ffvelrnd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` ( B \ s ) ) e. ~P B )
73 72 elpwid 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` ( B \ s ) ) C_ B )
74 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 ) ) ) ) )
75 69 73 74 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 ) ) ) ) )
76 59 75 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 ) ) ) ) ) )
77 simp3 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> b = ( B \ t ) )
78 simp13 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> a = ( B \ s ) )
79 77 78 sseq12d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( b C_ a <-> ( B \ t ) C_ ( B \ s ) ) )
80 77 fveq2d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` b ) = ( I ` ( B \ t ) ) )
81 78 fveq2d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I ` a ) = ( I ` ( B \ s ) ) )
82 80 81 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 ) ) ) )
83 79 82 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 ) ) ) ) )
84 1 2 3 ntrclsfv1 
 |-  ( ph -> ( D ` I ) = K )
85 60 84 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( D ` I ) = K )
86 85 fveq1d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( D ` I ) ` s ) = ( K ` s ) )
87 eqid 
 |-  ( D ` I ) = ( D ` I )
88 eqid 
 |-  ( ( D ` I ) ` s ) = ( ( D ` I ) ` s )
89 1 2 65 62 87 53 88 dssmapfv3d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( D ` I ) ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
90 86 89 eqtr3d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( K ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
91 60 3 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> I D K )
92 1 2 91 ntrclsfv1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( D ` I ) = K )
93 92 fveq1d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( D ` I ) ` t ) = ( K ` t ) )
94 eqid 
 |-  ( ( D ` I ) ` t ) = ( ( D ` I ) ` t )
95 1 2 65 62 87 55 94 dssmapfv3d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( D ` I ) ` t ) = ( B \ ( I ` ( B \ t ) ) ) )
96 93 95 eqtr3d 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( K ` t ) = ( B \ ( I ` ( B \ t ) ) ) )
97 90 96 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 ) ) ) ) )
98 97 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 ) ) ) ) ) )
99 76 83 98 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 ) ) ) )
100 37 52 99 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 ) ) ) )
101 19 33 100 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 ) ) ) )
102 14 101 syl5bb 
 |-  ( 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 ) ) ) )