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 elmapi ⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
71 70 adantr ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
72 simpr ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
73 difssd ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → ( 𝐵 ∖ 𝑠 ) ⊆ 𝐵 )
74 72 73 sselpwd ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
75 71 74 ffvelcdmd ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∈ 𝒫 𝐵 )
76 75 elpwid ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 )
77 orc ⊢ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 ∨ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ⊆ 𝐵 ) )
78 inss ⊢ ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 ∨ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ⊆ 𝐵 ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ 𝐵 )
79 76 77 78 3syl ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ 𝐵 )
80 difssd ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ⊆ 𝐵 )
81 72 80 sselpwd ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ∈ 𝒫 𝐵 )
82 71 81 ffvelcdmd ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ∈ 𝒫 𝐵 )
83 82 elpwid ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ⊆ 𝐵 )
84 79 83 jca ⊢ ( ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐵 ∈ V ) → ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ 𝐵 ∧ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ⊆ 𝐵 ) )
85 sscon34b ⊢ ( ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ 𝐵 ∧ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ⊆ 𝐵 ) → ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) ⊆ ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
86 67 69 84 85 4syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) ⊆ ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
87 difindi ⊢ ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
88 87 sseq2i ⊢ ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) ⊆ ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) ⊆ ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
89 88 a1i ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) ⊆ ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) ⊆ ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
90 67 15 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝐵 ∈ V )
91 67 68 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
92 simp12 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑠 ∈ 𝒫 𝐵 )
93 rp-simp2 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑡 ∈ 𝒫 𝐵 )
94 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝐵 ∈ V )
95 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
96 eqid ⊢ ( 𝐷 ‘ 𝐼 ) = ( 𝐷 ‘ 𝐼 )
97 simpl ⊢ ( ( 𝐵 ∈ V ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝐵 ∈ V )
98 simprl ⊢ ( ( 𝐵 ∈ V ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝑠 ∈ 𝒫 𝐵 )
99 98 elpwid ⊢ ( ( 𝐵 ∈ V ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝑠 ⊆ 𝐵 )
100 simprr ⊢ ( ( 𝐵 ∈ V ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝑡 ∈ 𝒫 𝐵 )
101 100 elpwid ⊢ ( ( 𝐵 ∈ V ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝑡 ⊆ 𝐵 )
102 99 101 unssd ⊢ ( ( 𝐵 ∈ V ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( 𝑠 ∪ 𝑡 ) ⊆ 𝐵 )
103 97 102 sselpwd ⊢ ( ( 𝐵 ∈ V ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( 𝑠 ∪ 𝑡 ) ∈ 𝒫 𝐵 )
104 103 3ad2antl2 ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( 𝑠 ∪ 𝑡 ) ∈ 𝒫 𝐵 )
105 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) )
106 1 2 94 95 96 104 105 dssmapfv3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) )
107 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝜑 )
108 1 2 3 ntrclsfv1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐼 ) = 𝐾 )
109 108 fveq1d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) ) = ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) )
110 107 109 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ ( 𝑠 ∪ 𝑡 ) ) = ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) )
111 106 110 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) = ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) )
112 simprl ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝑠 ∈ 𝒫 𝐵 )
113 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 )
114 1 2 94 95 96 112 113 dssmapfv3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
115 108 fveq1d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐾 ‘ 𝑠 ) )
116 107 115 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐾 ‘ 𝑠 ) )
117 114 116 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) = ( 𝐾 ‘ 𝑠 ) )
118 simprr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → 𝑡 ∈ 𝒫 𝐵 )
119 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 )
120 1 2 94 95 96 118 119 dssmapfv3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
121 108 fveq1d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( 𝐾 ‘ 𝑡 ) )
122 107 121 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( 𝐾 ‘ 𝑡 ) )
123 120 122 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ( 𝐾 ‘ 𝑡 ) )
124 117 123 uneq12d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) )
125 111 124 sseq12d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) ) → ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) ⊆ ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ↔ ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
126 67 90 91 92 93 125 syl32anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ) ⊆ ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) ↔ ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
127 86 89 126 3bitrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) ) ↔ ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
128 58 66 127 3bitrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) ⊆ ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) ↔ ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
129 36 51 128 ralxfrd2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) → ( ∀ 𝑏 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) ⊆ ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
130 18 32 129 ralxfrd2 ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝒫 𝐵 ∀ 𝑏 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) ⊆ ( 𝐼 ‘ ( 𝑎 ∩ 𝑏 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )
131 14 130 bitrid ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) ) )