Metamath Proof Explorer


Theorem ntrclsk3

Description: The intersection of interiors of a every pair is a subset of the interior of the intersection of the pair if an only if the closure of the union of every pair is a subset of the union of closures of the pair. (Contributed by RP, 19-Jun-2021)

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

Proof

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