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 V k 𝒫 i 𝒫 i j 𝒫 i i k i j
ntrcls.d D = O B
ntrcls.r φ I D K
Assertion ntrclsiso φ s 𝒫 B t 𝒫 B s t I s I t s 𝒫 B t 𝒫 B s t K s K t

Proof

Step Hyp Ref Expression
1 ntrcls.o O = i V k 𝒫 i 𝒫 i j 𝒫 i i k i j
2 ntrcls.d D = O B
3 ntrcls.r φ I D K
4 sseq1 s = b s t b t
5 fveq2 s = b I s = I b
6 5 sseq1d s = b I s I t I b I t
7 4 6 imbi12d s = b s t I s I t b t I b I t
8 sseq2 t = a b t b a
9 fveq2 t = a I t = I a
10 9 sseq2d t = a I b I t I b I a
11 8 10 imbi12d t = a b t I b I t b a I b I a
12 7 11 cbvral2vw s 𝒫 B t 𝒫 B s t I s I t b 𝒫 B a 𝒫 B b a I b I a
13 ralcom b 𝒫 B a 𝒫 B b a I b I a a 𝒫 B b 𝒫 B b a I b I a
14 12 13 bitri s 𝒫 B t 𝒫 B s t I s I t a 𝒫 B b 𝒫 B b a I b I a
15 simpl φ s 𝒫 B φ
16 2 3 ntrclsbex φ B V
17 15 16 syl φ s 𝒫 B B V
18 difssd φ s 𝒫 B B s B
19 17 18 sselpwd φ s 𝒫 B B s 𝒫 B
20 elpwi a 𝒫 B a B
21 simpl B V a B B V
22 difssd B V a B B a B
23 21 22 sselpwd B V a B B a 𝒫 B
24 simpr B V a B s = B a s = B a
25 24 difeq2d B V a B s = B a B s = B B a
26 25 eqeq2d B V a 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 V a B s = B a a = B s B B a = a
29 dfss4 a B B B a = a
30 29 biimpi a B B B a = a
31 30 adantl B V a B B B a = a
32 23 28 31 rspcedvd B V a B s 𝒫 B a = B s
33 16 20 32 syl2an φ a 𝒫 B s 𝒫 B a = B s
34 simpl1 φ s 𝒫 B a = B s t 𝒫 B φ
35 34 16 syl φ s 𝒫 B a = B s t 𝒫 B B V
36 difssd φ s 𝒫 B a = B s t 𝒫 B B t B
37 35 36 sselpwd φ s 𝒫 B a = B s t 𝒫 B B t 𝒫 B
38 elpwi b 𝒫 B b B
39 simpl B V b B B V
40 difssd B V b B B b B
41 39 40 sselpwd B V b B B b 𝒫 B
42 simpr B V b B t = B b t = B b
43 42 difeq2d B V b B t = B b B t = B B b
44 43 eqeq2d B V b 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 V b B t = B b b = B t B B b = b
47 dfss4 b B B B b = b
48 47 biimpi b B B B b = b
49 48 adantl B V b B B B b = b
50 41 46 49 rspcedvd B V b B t 𝒫 B b = B t
51 16 38 50 syl2an φ b 𝒫 B t 𝒫 B b = B t
52 51 3ad2antl1 φ s 𝒫 B a = B s b 𝒫 B t 𝒫 B b = B t
53 simp12 φ s 𝒫 B a = B s t 𝒫 B b = B t s 𝒫 B
54 53 elpwid φ s 𝒫 B a = B s t 𝒫 B b = B t s B
55 simp2 φ s 𝒫 B a = B s t 𝒫 B b = B t t 𝒫 B
56 55 elpwid φ s 𝒫 B a = B s t 𝒫 B b = B t t B
57 sscon34b s B t B s t B t B s
58 54 56 57 syl2anc φ s 𝒫 B a = B s t 𝒫 B b = B t s t B t B s
59 58 bicomd φ s 𝒫 B a = B s t 𝒫 B b = B t B t B s s t
60 simp11 φ s 𝒫 B a = B s t 𝒫 B b = B t φ
61 1 2 3 ntrclsiex φ I 𝒫 B 𝒫 B
62 60 61 syl φ s 𝒫 B a = B s t 𝒫 B b = B t I 𝒫 B 𝒫 B
63 elmapi I 𝒫 B 𝒫 B I : 𝒫 B 𝒫 B
64 62 63 syl φ s 𝒫 B a = B s t 𝒫 B b = B t I : 𝒫 B 𝒫 B
65 60 16 syl φ s 𝒫 B a = B s t 𝒫 B b = B t B V
66 difssd φ s 𝒫 B a = B s t 𝒫 B b = B t B t B
67 65 66 sselpwd φ s 𝒫 B a = B s t 𝒫 B b = B t B t 𝒫 B
68 64 67 ffvelrnd φ s 𝒫 B a = B s t 𝒫 B b = B t I B t 𝒫 B
69 68 elpwid φ s 𝒫 B a = B s t 𝒫 B b = B t I B t B
70 difssd φ s 𝒫 B a = B s t 𝒫 B b = B t B s B
71 65 70 sselpwd φ s 𝒫 B a = B s t 𝒫 B b = B t B s 𝒫 B
72 64 71 ffvelrnd φ s 𝒫 B a = B s t 𝒫 B b = B t I B s 𝒫 B
73 72 elpwid φ s 𝒫 B a = B s t 𝒫 B b = B t I B s B
74 sscon34b I B t B I B s B I B t I B s B I B s B I B t
75 69 73 74 syl2anc φ s 𝒫 B a = B s t 𝒫 B b = B t I B t I B s B I B s B I B t
76 59 75 imbi12d φ s 𝒫 B a = B s t 𝒫 B b = B t B t B s I B t I B s s t B I B s B I B t
77 simp3 φ s 𝒫 B a = B s t 𝒫 B b = B t b = B t
78 simp13 φ s 𝒫 B a = B s t 𝒫 B b = B t a = B s
79 77 78 sseq12d φ s 𝒫 B a = B s t 𝒫 B b = B t b a B t B s
80 77 fveq2d φ s 𝒫 B a = B s t 𝒫 B b = B t I b = I B t
81 78 fveq2d φ s 𝒫 B a = B s t 𝒫 B b = B t I a = I B s
82 80 81 sseq12d φ s 𝒫 B a = B s t 𝒫 B b = B t I b I a I B t I B s
83 79 82 imbi12d φ s 𝒫 B a = B s t 𝒫 B b = B t b a I b I a B t B s I B t I B s
84 1 2 3 ntrclsfv1 φ D I = K
85 60 84 syl φ s 𝒫 B a = B s t 𝒫 B b = B t D I = K
86 85 fveq1d φ s 𝒫 B a = B s t 𝒫 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 φ s 𝒫 B a = B s t 𝒫 B b = B t D I s = B I B s
90 86 89 eqtr3d φ s 𝒫 B a = B s t 𝒫 B b = B t K s = B I B s
91 60 3 syl φ s 𝒫 B a = B s t 𝒫 B b = B t I D K
92 1 2 91 ntrclsfv1 φ s 𝒫 B a = B s t 𝒫 B b = B t D I = K
93 92 fveq1d φ s 𝒫 B a = B s t 𝒫 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 φ s 𝒫 B a = B s t 𝒫 B b = B t D I t = B I B t
96 93 95 eqtr3d φ s 𝒫 B a = B s t 𝒫 B b = B t K t = B I B t
97 90 96 sseq12d φ s 𝒫 B a = B s t 𝒫 B b = B t K s K t B I B s B I B t
98 97 imbi2d φ s 𝒫 B a = B s t 𝒫 B b = B t s t K s K t s t B I B s B I B t
99 76 83 98 3bitr4d φ s 𝒫 B a = B s t 𝒫 B b = B t b a I b I a s t K s K t
100 37 52 99 ralxfrd2 φ s 𝒫 B a = B s b 𝒫 B b a I b I a t 𝒫 B s t K s K t
101 19 33 100 ralxfrd2 φ a 𝒫 B b 𝒫 B b a I b I a s 𝒫 B t 𝒫 B s t K s K t
102 14 101 syl5bb φ s 𝒫 B t 𝒫 B s t I s I t s 𝒫 B t 𝒫 B s t K s K t