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 ffvelcdmd ⊒ ( ( 𝐼 ∈ ( 𝒫 𝐡 ↑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 ffvelcdmd ⊒ ( ( 𝐼 ∈ ( 𝒫 𝐡 ↑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 bitrid ⊒ ( πœ‘ β†’ ( βˆ€ 𝑠 ∈ 𝒫 𝐡 βˆ€ 𝑑 ∈ 𝒫 𝐡 ( ( 𝐼 β€˜ 𝑠 ) ∩ ( 𝐼 β€˜ 𝑑 ) ) βŠ† ( 𝐼 β€˜ ( 𝑠 ∩ 𝑑 ) ) ↔ βˆ€ 𝑠 ∈ 𝒫 𝐡 βˆ€ 𝑑 ∈ 𝒫 𝐡 ( 𝐾 β€˜ ( 𝑠 βˆͺ 𝑑 ) ) βŠ† ( ( 𝐾 β€˜ 𝑠 ) βˆͺ ( 𝐾 β€˜ 𝑑 ) ) ) )