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 ⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
ntrcls.d ⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
ntrcls.r ⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
Assertion ntrclsiso ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o ⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
2 ntrcls.d ⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3 ntrcls.r ⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
4 sseq1 ⊢ ( 𝑠 = 𝑏 → ( 𝑠 ⊆ 𝑡 ↔ 𝑏 ⊆ 𝑡 ) )
5 fveq2 ⊢ ( 𝑠 = 𝑏 → ( 𝐼 ‘ 𝑠 ) = ( 𝐼 ‘ 𝑏 ) )
6 5 sseq1d ⊢ ( 𝑠 = 𝑏 → ( ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ↔ ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) )
7 4 6 imbi12d ⊢ ( 𝑠 = 𝑏 → ( ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑏 ⊆ 𝑡 → ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ) )
8 sseq2 ⊢ ( 𝑡 = 𝑎 → ( 𝑏 ⊆ 𝑡 ↔ 𝑏 ⊆ 𝑎 ) )
9 fveq2 ⊢ ( 𝑡 = 𝑎 → ( 𝐼 ‘ 𝑡 ) = ( 𝐼 ‘ 𝑎 ) )
10 9 sseq2d ⊢ ( 𝑡 = 𝑎 → ( ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑡 ) ↔ ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑎 ) ) )
11 8 10 imbi12d ⊢ ( 𝑡 = 𝑎 → ( ( 𝑏 ⊆ 𝑡 → ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑏 ⊆ 𝑎 → ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑎 ) ) ) )
12 7 11 cbvral2vw ⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑏 ∈ 𝒫 𝐵 ∀ 𝑎 ∈ 𝒫 𝐵 ( 𝑏 ⊆ 𝑎 → ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑎 ) ) )
13 ralcom ⊢ ( ∀ 𝑏 ∈ 𝒫 𝐵 ∀ 𝑎 ∈ 𝒫 𝐵 ( 𝑏 ⊆ 𝑎 → ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑎 ) ) ↔ ∀ 𝑎 ∈ 𝒫 𝐵 ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝑏 ⊆ 𝑎 → ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑎 ) ) )
14 12 13 bitri ⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑎 ∈ 𝒫 𝐵 ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝑏 ⊆ 𝑎 → ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑎 ) ) )
15 simpl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝜑 )
16 2 3 ntrclsbex ⊢ ( 𝜑 → 𝐵 ∈ V )
17 15 16 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝐵 ∈ V )
18 difssd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑠 ) ⊆ 𝐵 )
19 17 18 sselpwd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
20 elpwi ⊢ ( 𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵 )
21 simpl ⊢ ( ( 𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵 ) → 𝐵 ∈ V )
22 difssd ⊢ ( ( 𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝑎 ) ⊆ 𝐵 )
23 21 22 sselpwd ⊢ ( ( 𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝑎 ) ∈ 𝒫 𝐵 )
24 simpr ⊢ ( ( ( 𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵 ) ∧ 𝑠 = ( 𝐵 ∖ 𝑎 ) ) → 𝑠 = ( 𝐵 ∖ 𝑎 ) )
25 24 difeq2d ⊢ ( ( ( 𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵 ) ∧ 𝑠 = ( 𝐵 ∖ 𝑎 ) ) → ( 𝐵 ∖ 𝑠 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) )
26 25 eqeq2d ⊢ ( ( ( 𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵 ) ∧ 𝑠 = ( 𝐵 ∖ 𝑎 ) ) → ( 𝑎 = ( 𝐵 ∖ 𝑠 ) ↔ 𝑎 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) ) )
27 eqcom ⊢ ( 𝑎 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 )
28 26 27 bitrdi ⊢ ( ( ( 𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵 ) ∧ 𝑠 = ( 𝐵 ∖ 𝑎 ) ) → ( 𝑎 = ( 𝐵 ∖ 𝑠 ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 ) )
29 dfss4 ⊢ ( 𝑎 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 )
30 29 biimpi ⊢ ( 𝑎 ⊆ 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 )
31 30 adantl ⊢ ( ( 𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 )
32 23 28 31 rspcedvd ⊢ ( ( 𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵 ) → ∃ 𝑠 ∈ 𝒫 𝐵 𝑎 = ( 𝐵 ∖ 𝑠 ) )
33 16 20 32 syl2an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐵 ) → ∃ 𝑠 ∈ 𝒫 𝐵 𝑎 = ( 𝐵 ∖ 𝑠 ) )
34 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝜑 )
35 34 16 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐵 ∈ V )
36 difssd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑡 ) ⊆ 𝐵 )
37 35 36 sselpwd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
38 elpwi ⊢ ( 𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵 )
39 simpl ⊢ ( ( 𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵 ) → 𝐵 ∈ V )
40 difssd ⊢ ( ( 𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝑏 ) ⊆ 𝐵 )
41 39 40 sselpwd ⊢ ( ( 𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝑏 ) ∈ 𝒫 𝐵 )
42 simpr ⊢ ( ( ( 𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵 ) ∧ 𝑡 = ( 𝐵 ∖ 𝑏 ) ) → 𝑡 = ( 𝐵 ∖ 𝑏 ) )
43 42 difeq2d ⊢ ( ( ( 𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵 ) ∧ 𝑡 = ( 𝐵 ∖ 𝑏 ) ) → ( 𝐵 ∖ 𝑡 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) )
44 43 eqeq2d ⊢ ( ( ( 𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵 ) ∧ 𝑡 = ( 𝐵 ∖ 𝑏 ) ) → ( 𝑏 = ( 𝐵 ∖ 𝑡 ) ↔ 𝑏 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) ) )
45 eqcom ⊢ ( 𝑏 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 )
46 44 45 bitrdi ⊢ ( ( ( 𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵 ) ∧ 𝑡 = ( 𝐵 ∖ 𝑏 ) ) → ( 𝑏 = ( 𝐵 ∖ 𝑡 ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 ) )
47 dfss4 ⊢ ( 𝑏 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 )
48 47 biimpi ⊢ ( 𝑏 ⊆ 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 )
49 48 adantl ⊢ ( ( 𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 )
50 41 46 49 rspcedvd ⊢ ( ( 𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵 ) → ∃ 𝑡 ∈ 𝒫 𝐵 𝑏 = ( 𝐵 ∖ 𝑡 ) )
51 16 38 50 syl2an ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝒫 𝐵 ) → ∃ 𝑡 ∈ 𝒫 𝐵 𝑏 = ( 𝐵 ∖ 𝑡 ) )
52 51 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑏 ∈ 𝒫 𝐵 ) → ∃ 𝑡 ∈ 𝒫 𝐵 𝑏 = ( 𝐵 ∖ 𝑡 ) )
53 simp12 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑠 ∈ 𝒫 𝐵 )
54 53 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑠 ⊆ 𝐵 )
55 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑡 ∈ 𝒫 𝐵 )
56 55 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑡 ⊆ 𝐵 )
57 sscon34b ⊢ ( ( 𝑠 ⊆ 𝐵 ∧ 𝑡 ⊆ 𝐵 ) → ( 𝑠 ⊆ 𝑡 ↔ ( 𝐵 ∖ 𝑡 ) ⊆ ( 𝐵 ∖ 𝑠 ) ) )
58 54 56 57 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝑠 ⊆ 𝑡 ↔ ( 𝐵 ∖ 𝑡 ) ⊆ ( 𝐵 ∖ 𝑠 ) ) )
59 58 bicomd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐵 ∖ 𝑡 ) ⊆ ( 𝐵 ∖ 𝑠 ) ↔ 𝑠 ⊆ 𝑡 ) )
60 simp11 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝜑 )
61 1 2 3 ntrclsiex ⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
62 60 61 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
63 elmapi ⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
64 62 63 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
65 60 16 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝐵 ∈ V )
66 difssd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐵 ∖ 𝑡 ) ⊆ 𝐵 )
67 65 66 sselpwd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
68 64 67 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ∈ 𝒫 𝐵 )
69 68 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ⊆ 𝐵 )
70 difssd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐵 ∖ 𝑠 ) ⊆ 𝐵 )
71 65 70 sselpwd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
72 64 71 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∈ 𝒫 𝐵 )
73 72 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 )
74 sscon34b ⊢ ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ⊆ 𝐵 ∧ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
75 69 73 74 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
76 59 75 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( ( 𝐵 ∖ 𝑡 ) ⊆ ( 𝐵 ∖ 𝑠 ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ↔ ( 𝑠 ⊆ 𝑡 → ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
77 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑏 = ( 𝐵 ∖ 𝑡 ) )
78 simp13 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑎 = ( 𝐵 ∖ 𝑠 ) )
79 77 78 sseq12d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝑏 ⊆ 𝑎 ↔ ( 𝐵 ∖ 𝑡 ) ⊆ ( 𝐵 ∖ 𝑠 ) ) )
80 77 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐼 ‘ 𝑏 ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) )
81 78 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐼 ‘ 𝑎 ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) )
82 80 81 sseq12d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑎 ) ↔ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
83 79 82 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝑏 ⊆ 𝑎 → ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑎 ) ) ↔ ( ( 𝐵 ∖ 𝑡 ) ⊆ ( 𝐵 ∖ 𝑠 ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
84 1 2 3 ntrclsfv1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐼 ) = 𝐾 )
85 60 84 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐷 ‘ 𝐼 ) = 𝐾 )
86 85 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐾 ‘ 𝑠 ) )
87 eqid ⊢ ( 𝐷 ‘ 𝐼 ) = ( 𝐷 ‘ 𝐼 )
88 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 )
89 1 2 65 62 87 53 88 dssmapfv3d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
90 86 89 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐾 ‘ 𝑠 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
91 60 3 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝐼 𝐷 𝐾 )
92 1 2 91 ntrclsfv1 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐷 ‘ 𝐼 ) = 𝐾 )
93 92 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( 𝐾 ‘ 𝑡 ) )
94 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 )
95 1 2 65 62 87 55 94 dssmapfv3d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
96 93 95 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐾 ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
97 90 96 sseq12d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
98 97 imbi2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝑠 ⊆ 𝑡 → ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ↔ ( 𝑠 ⊆ 𝑡 → ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
99 76 83 98 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝑏 ⊆ 𝑎 → ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑎 ) ) ↔ ( 𝑠 ⊆ 𝑡 → ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ) )
100 37 52 99 ralxfrd2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) → ( ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝑏 ⊆ 𝑎 → ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑎 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ) )
101 19 33 100 ralxfrd2 ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝒫 𝐵 ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝑏 ⊆ 𝑎 → ( 𝐼 ‘ 𝑏 ) ⊆ ( 𝐼 ‘ 𝑎 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ) )
102 14 101 bitrid ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ) )