Metamath Proof Explorer

Theorem ntrclsk13

Description: The interior of the intersection of any pair is equal to the intersection of the interiors if and only if the closure of the unions of any pair is equal to the union of closures. (Contributed by RP, 19-Jun-2021)

Ref Expression
Hypotheses ntrcls.o ⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
ntrcls.d ⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
ntrcls.r ⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
Assertion ntrclsk13 ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o ⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
2 ntrcls.d ⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3 ntrcls.r ⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
4 ineq1 ⊢ ( 𝑠 = 𝑎 → ( 𝑠 ∩ 𝑡 ) = ( 𝑎 ∩ 𝑡 ) )
5 4 fveq2d ⊢ ( 𝑠 = 𝑎 → ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( 𝐼 ‘ ( 𝑎 ∩ 𝑡 ) ) )
6 fveq2 ⊢ ( 𝑠 = 𝑎 → ( 𝐼 ‘ 𝑠 ) = ( 𝐼 ‘ 𝑎 ) )
7 6 ineq1d ⊢ ( 𝑠 = 𝑎 → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑡 ) ) )
8 5 7 eqeq12d ⊢ ( 𝑠 = 𝑎 → ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝐼 ‘ ( 𝑎 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ) )
9 ineq2 ⊢ ( 𝑡 = 𝑏 → ( 𝑎 ∩ 𝑡 ) = ( 𝑎 ∩ 𝑏 ) )
10 9 fveq2d ⊢ ( 𝑡 = 𝑏 → ( 𝐼 ‘ ( 𝑎 ∩ 𝑡 ) ) = ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) )
11 fveq2 ⊢ ( 𝑡 = 𝑏 → ( 𝐼 ‘ 𝑡 ) = ( 𝐼 ‘ 𝑏 ) )
12 11 ineq2d ⊢ ( 𝑡 = 𝑏 → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) )
13 10 12 eqeq12d ⊢ ( 𝑡 = 𝑏 → ( ( 𝐼 ‘ ( 𝑎 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) ) )
14 8 13 cbvral2vw ⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑎 ∈ 𝒫 𝐵 ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) )
15 2 3 ntrclsbex ⊢ ( 𝜑 → 𝐵 ∈ V )
16 difssd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑠 ) ⊆ 𝐵 )
17 15 16 sselpwd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
19 elpwi ⊢ ( 𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵 )
20 15 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐵 ) → 𝐵 ∈ V )
21 difssd ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝑎 ) ⊆ 𝐵 )
22 20 21 sselpwd ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝑎 ) ∈ 𝒫 𝐵 )
23 difeq2 ⊢ ( 𝑠 = ( 𝐵 ∖ 𝑎 ) → ( 𝐵 ∖ 𝑠 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) )
24 23 eqeq2d ⊢ ( 𝑠 = ( 𝐵 ∖ 𝑎 ) → ( 𝑎 = ( 𝐵 ∖ 𝑠 ) ↔ 𝑎 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) ) )
25 eqcom ⊢ ( 𝑎 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 )
26 24 25 bitrdi ⊢ ( 𝑠 = ( 𝐵 ∖ 𝑎 ) → ( 𝑎 = ( 𝐵 ∖ 𝑠 ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 ) )
27 26 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐵 ) ∧ 𝑠 = ( 𝐵 ∖ 𝑎 ) ) → ( 𝑎 = ( 𝐵 ∖ 𝑠 ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 ) )
28 dfss4 ⊢ ( 𝑎 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 )
29 28 biimpi ⊢ ( 𝑎 ⊆ 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 )
31 22 27 30 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐵 ) → ∃ 𝑠 ∈ 𝒫 𝐵 𝑎 = ( 𝐵 ∖ 𝑠 ) )
32 19 31 sylan2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐵 ) → ∃ 𝑠 ∈ 𝒫 𝐵 𝑎 = ( 𝐵 ∖ 𝑠 ) )
33 ineq1 ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( 𝑎 ∩ 𝑏 ) = ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) )
34 33 fveq2d ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) = ( 𝐼 ‘ ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) ) )
35 fveq2 ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( 𝐼 ‘ 𝑎 ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) )
36 35 ineq1d ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) )
37 34 36 eqeq12d ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) ↔ ( 𝐼 ‘ ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) ) )
38 37 ralbidv ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) ↔ ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) ) )
39 38 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) → ( ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) ↔ ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) ) )
40 difssd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑡 ) ⊆ 𝐵 )
41 15 40 sselpwd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
42 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
43 simpll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑏 ∈ 𝒫 𝐵 ) → 𝜑 )
44 elpwi ⊢ ( 𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵 )
45 44 adantl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑏 ∈ 𝒫 𝐵 ) → 𝑏 ⊆ 𝐵 )
46 difssd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑏 ) ⊆ 𝐵 )
47 15 46 sselpwd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑏 ) ∈ 𝒫 𝐵 )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝑏 ) ∈ 𝒫 𝐵 )
49 difeq2 ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑏 ) → ( 𝐵 ∖ 𝑡 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) )
50 49 eqeq2d ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑏 ) → ( 𝑏 = ( 𝐵 ∖ 𝑡 ) ↔ 𝑏 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) ) )
51 eqcom ⊢ ( 𝑏 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 )
52 50 51 bitrdi ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑏 ) → ( 𝑏 = ( 𝐵 ∖ 𝑡 ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 ) )
53 52 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐵 ) ∧ 𝑡 = ( 𝐵 ∖ 𝑏 ) ) → ( 𝑏 = ( 𝐵 ∖ 𝑡 ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 ) )
54 dfss4 ⊢ ( 𝑏 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 )
55 54 biimpi ⊢ ( 𝑏 ⊆ 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 )
56 55 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 )
57 48 53 56 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐵 ) → ∃ 𝑡 ∈ 𝒫 𝐵 𝑏 = ( 𝐵 ∖ 𝑡 ) )
58 43 45 57 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑏 ∈ 𝒫 𝐵 ) → ∃ 𝑡 ∈ 𝒫 𝐵 𝑏 = ( 𝐵 ∖ 𝑡 ) )
59 ineq2 ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) = ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) ) )
60 difundi ⊢ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) )
61 59 60 eqtr4di ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) = ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) )
62 61 fveq2d ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( 𝐼 ‘ ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) ) = ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) )
63 fveq2 ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( 𝐼 ‘ 𝑏 ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) )
64 63 ineq2d ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
65 62 64 eqeq12d ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( ( 𝐼 ‘ ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) ↔ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
66 65 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐼 ‘ ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) ↔ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
67 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝜑 )
68 67 15 jccir ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝜑 ∧ 𝐵 ∈ V ) )
69 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑠 ∈ 𝒫 𝐵 )
70 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑡 ∈ 𝒫 𝐵 )
71 1 2 3 ntrclsiex ⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
72 elmapi ⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
73 71 72 syl ⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
74 73 anim1i ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) )
75 74 adantr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) )
76 simpl ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
77 simpr ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
78 difssd ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ⊆ 𝐵 )
79 77 78 sselpwd ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ∈ 𝒫 𝐵 )
80 76 79 ffvelcdmd ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ∈ 𝒫 𝐵 )
81 80 elpwid ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ⊆ 𝐵 )
82 difssd ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → ( 𝐵 ∖ 𝑠 ) ⊆ 𝐵 )
83 77 82 sselpwd ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
84 76 83 ffvelcdmd ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∈ 𝒫 𝐵 )
85 84 elpwid ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 )
86 ssinss1 ⊢ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ 𝐵 )
87 85 86 syl ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ 𝐵 )
88 81 87 jca ⊢ ( ( 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ∧ 𝐵 ∈ V ) → ( ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ⊆ 𝐵 ∧ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ 𝐵 ) )
89 rcompleq ⊢ ( ( ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ⊆ 𝐵 ∧ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ 𝐵 ) → ( ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) = ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
90 75 88 89 3syl ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) = ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
91 simplr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝐵 ∈ V )
92 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
93 eqid ⊢ ( 𝐷 ‘ 𝐼 ) = ( 𝐷 ‘ 𝐼 )
94 simprl ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝑠 ∈ 𝒫 𝐵 )
95 94 elpwid ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝑠 ⊆ 𝐵 )
96 simprr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝑡 ∈ 𝒫 𝐵 )
97 96 elpwid ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝑡 ⊆ 𝐵 )
98 95 97 unssd ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( 𝑠 ∪ 𝑡 ) ⊆ 𝐵 )
99 91 98 sselpwd ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( 𝑠 ∪ 𝑡 ) ∈ 𝒫 𝐵 )
100 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) )
101 1 2 91 92 93 99 100 dssmapfv3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) )
102 simpl ⊢ ( ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
103 simplr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝐵 ∈ V )
104 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
105 simpr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
106 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 )
107 1 2 103 104 93 105 106 dssmapfv3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
108 102 107 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
109 simpr ⊢ ( ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
110 simplr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐵 ∈ V )
111 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
112 simpr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
113 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 )
114 1 2 110 111 93 112 113 dssmapfv3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
115 109 114 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
116 108 115 uneq12d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ∪ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) ) = ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
117 difindi ⊢ ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
118 116 117 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ∪ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) ) = ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
119 101 118 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ∪ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) = ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
120 simpll ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝜑 )
121 1 2 3 ntrclsfv1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐼 ) = 𝐾 )
122 fveq1 ⊢ ( ( 𝐷 ‘ 𝐼 ) = 𝐾 → ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) ) = ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) )
123 fveq1 ⊢ ( ( 𝐷 ‘ 𝐼 ) = 𝐾 → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐾 ‘ 𝑠 ) )
124 fveq1 ⊢ ( ( 𝐷 ‘ 𝐼 ) = 𝐾 → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( 𝐾 ‘ 𝑡 ) )
125 123 124 uneq12d ⊢ ( ( 𝐷 ‘ 𝐼 ) = 𝐾 → ( ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ∪ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) )
126 122 125 eqeq12d ⊢ ( ( 𝐷 ‘ 𝐼 ) = 𝐾 → ( ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ∪ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) ) ↔ ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
127 120 121 126 3syl ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ∪ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) ) ↔ ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
128 90 119 127 3bitr2d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ↔ ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
129 68 69 70 128 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ↔ ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
130 66 129 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐼 ‘ ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) ↔ ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
131 42 58 130 ralxfrd2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
132 131 3adant3 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) → ( ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
133 39 132 bitrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) → ( ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
134 18 32 133 ralxfrd2 ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝒫 𝐵 ∀ 𝑏 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
135 14 134 bitrid ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )