Metamath Proof Explorer

Theorem ntrclskb

Description: The interiors of disjoint sets are disjoint if and only if the closures of sets that span the base set also span the base set. (Contributed by RP, 10-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 ntrcls.o ⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
2 ntrcls.d ⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3 ntrcls.r ⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
4 ineq1 ⊢ ( 𝑠 = 𝑎 → ( 𝑠 ∩ 𝑡 ) = ( 𝑎 ∩ 𝑡 ) )
5 4 eqeq1d ⊢ ( 𝑠 = 𝑎 → ( ( 𝑠 ∩ 𝑡 ) = ∅ ↔ ( 𝑎 ∩ 𝑡 ) = ∅ ) )
6 fveq2 ⊢ ( 𝑠 = 𝑎 → ( 𝐼 ‘ 𝑠 ) = ( 𝐼 ‘ 𝑎 ) )
7 6 ineq1d ⊢ ( 𝑠 = 𝑎 → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑡 ) ) )
8 7 eqeq1d ⊢ ( 𝑠 = 𝑎 → ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ↔ ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) )
9 5 8 imbi12d ⊢ ( 𝑠 = 𝑎 → ( ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( 𝑎 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) )
10 ineq2 ⊢ ( 𝑡 = 𝑏 → ( 𝑎 ∩ 𝑡 ) = ( 𝑎 ∩ 𝑏 ) )
11 10 eqeq1d ⊢ ( 𝑡 = 𝑏 → ( ( 𝑎 ∩ 𝑡 ) = ∅ ↔ ( 𝑎 ∩ 𝑏 ) = ∅ ) )
12 fveq2 ⊢ ( 𝑡 = 𝑏 → ( 𝐼 ‘ 𝑡 ) = ( 𝐼 ‘ 𝑏 ) )
13 12 ineq2d ⊢ ( 𝑡 = 𝑏 → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) )
14 13 eqeq1d ⊢ ( 𝑡 = 𝑏 → ( ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ↔ ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) )
15 11 14 imbi12d ⊢ ( 𝑡 = 𝑏 → ( ( ( 𝑎 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( 𝑎 ∩ 𝑏 ) = ∅ → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) ) )
16 9 15 cbvral2vw ⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ∀ 𝑎 ∈ 𝒫 𝐵 ∀ 𝑏 ∈ 𝒫 𝐵 ( ( 𝑎 ∩ 𝑏 ) = ∅ → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) )
17 2 3 ntrclsrcomplex ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
19 2 3 ntrclsrcomplex ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑎 ) ∈ 𝒫 𝐵 )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑎 ) ∈ 𝒫 𝐵 )
21 difeq2 ⊢ ( 𝑠 = ( 𝐵 ∖ 𝑎 ) → ( 𝐵 ∖ 𝑠 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) )
22 21 eqeq2d ⊢ ( 𝑠 = ( 𝐵 ∖ 𝑎 ) → ( 𝑎 = ( 𝐵 ∖ 𝑠 ) ↔ 𝑎 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) ) )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐵 ) ∧ 𝑠 = ( 𝐵 ∖ 𝑎 ) ) → ( 𝑎 = ( 𝐵 ∖ 𝑠 ) ↔ 𝑎 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) ) )
24 elpwi ⊢ ( 𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵 )
25 dfss4 ⊢ ( 𝑎 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 )
26 24 25 sylib ⊢ ( 𝑎 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) = 𝑎 )
27 26 eqcomd ⊢ ( 𝑎 ∈ 𝒫 𝐵 → 𝑎 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐵 ) → 𝑎 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑎 ) ) )
29 20 23 28 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐵 ) → ∃ 𝑠 ∈ 𝒫 𝐵 𝑎 = ( 𝐵 ∖ 𝑠 ) )
30 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝜑 )
31 2 3 ntrclsrcomplex ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
32 30 31 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
33 2 3 ntrclsrcomplex ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑏 ) ∈ 𝒫 𝐵 )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑏 ) ∈ 𝒫 𝐵 )
35 difeq2 ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑏 ) → ( 𝐵 ∖ 𝑡 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) )
36 35 eqeq2d ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑏 ) → ( 𝑏 = ( 𝐵 ∖ 𝑡 ) ↔ 𝑏 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) ) )
37 36 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝒫 𝐵 ) ∧ 𝑡 = ( 𝐵 ∖ 𝑏 ) ) → ( 𝑏 = ( 𝐵 ∖ 𝑡 ) ↔ 𝑏 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) ) )
38 elpwi ⊢ ( 𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵 )
39 dfss4 ⊢ ( 𝑏 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 )
40 38 39 sylib ⊢ ( 𝑏 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) = 𝑏 )
41 40 eqcomd ⊢ ( 𝑏 ∈ 𝒫 𝐵 → 𝑏 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) )
42 41 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝒫 𝐵 ) → 𝑏 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑏 ) ) )
43 34 37 42 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝒫 𝐵 ) → ∃ 𝑡 ∈ 𝒫 𝐵 𝑏 = ( 𝐵 ∖ 𝑡 ) )
44 43 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑏 ∈ 𝒫 𝐵 ) → ∃ 𝑡 ∈ 𝒫 𝐵 𝑏 = ( 𝐵 ∖ 𝑡 ) )
45 simp13 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑎 = ( 𝐵 ∖ 𝑠 ) )
46 ineq1 ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( 𝑎 ∩ 𝑏 ) = ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) )
47 46 eqeq1d ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( ( 𝑎 ∩ 𝑏 ) = ∅ ↔ ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) = ∅ ) )
48 fveq2 ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( 𝐼 ‘ 𝑎 ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) )
49 48 ineq1d ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) )
50 49 eqeq1d ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ↔ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) )
51 47 50 imbi12d ⊢ ( 𝑎 = ( 𝐵 ∖ 𝑠 ) → ( ( ( 𝑎 ∩ 𝑏 ) = ∅ → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) ↔ ( ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) = ∅ → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) ) )
52 45 51 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( ( 𝑎 ∩ 𝑏 ) = ∅ → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) ↔ ( ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) = ∅ → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) ) )
53 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑏 = ( 𝐵 ∖ 𝑡 ) )
54 ineq2 ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) = ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) ) )
55 54 eqeq1d ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) = ∅ ↔ ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) ) = ∅ ) )
56 fveq2 ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( 𝐼 ‘ 𝑏 ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) )
57 56 ineq2d ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
58 57 eqeq1d ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ↔ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ∅ ) )
59 55 58 imbi12d ⊢ ( 𝑏 = ( 𝐵 ∖ 𝑡 ) → ( ( ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) = ∅ → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) ↔ ( ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) ) = ∅ → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ∅ ) ) )
60 53 59 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( ( ( 𝐵 ∖ 𝑠 ) ∩ 𝑏 ) = ∅ → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) ↔ ( ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) ) = ∅ → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ∅ ) ) )
61 simp11 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝜑 )
62 simp12 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑠 ∈ 𝒫 𝐵 )
63 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → 𝑡 ∈ 𝒫 𝐵 )
64 simp2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
65 64 elpwid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑠 ⊆ 𝐵 )
66 simp3 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
67 66 elpwid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑡 ⊆ 𝐵 )
68 65 67 unssd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑠 ∪ 𝑡 ) ⊆ 𝐵 )
69 ssid ⊢ 𝐵 ⊆ 𝐵
70 rcompleq ⊢ ( ( ( 𝑠 ∪ 𝑡 ) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 ) → ( ( 𝑠 ∪ 𝑡 ) = 𝐵 ↔ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) = ( 𝐵 ∖ 𝐵 ) ) )
71 68 69 70 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝑠 ∪ 𝑡 ) = 𝐵 ↔ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) = ( 𝐵 ∖ 𝐵 ) ) )
72 difundi ⊢ ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) )
73 difid ⊢ ( 𝐵 ∖ 𝐵 ) = ∅
74 72 73 eqeq12i ⊢ ( ( 𝐵 ∖ ( 𝑠 ∪ 𝑡 ) ) = ( 𝐵 ∖ 𝐵 ) ↔ ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) ) = ∅ )
75 71 74 bitr2di ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) ) = ∅ ↔ ( 𝑠 ∪ 𝑡 ) = 𝐵 ) )
76 1 2 3 ntrclsiex ⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
77 76 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
78 elmapi ⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
79 77 78 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
80 2 3 ntrclsbex ⊢ ( 𝜑 → 𝐵 ∈ V )
81 80 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐵 ∈ V )
82 difssd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑠 ) ⊆ 𝐵 )
83 81 82 sselpwd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
84 79 83 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∈ 𝒫 𝐵 )
85 84 elpwid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 )
86 ssinss1 ⊢ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ 𝐵 )
87 85 86 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ 𝐵 )
88 0ss ⊢ ∅ ⊆ 𝐵
89 rcompleq ⊢ ( ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ⊆ 𝐵 ∧ ∅ ⊆ 𝐵 ) → ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ∅ ↔ ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = ( 𝐵 ∖ ∅ ) ) )
90 87 88 89 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ∅ ↔ ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = ( 𝐵 ∖ ∅ ) ) )
91 difindi ⊢ ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
92 dif0 ⊢ ( 𝐵 ∖ ∅ ) = 𝐵
93 91 92 eqeq12i ⊢ ( ( 𝐵 ∖ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = ( 𝐵 ∖ ∅ ) ↔ ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = 𝐵 )
94 90 93 bitrdi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ∅ ↔ ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = 𝐵 ) )
95 75 94 imbi12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) ) = ∅ → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ∅ ) ↔ ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = 𝐵 ) ) )
96 eqid ⊢ ( 𝐷 ‘ 𝐼 ) = ( 𝐷 ‘ 𝐼 )
97 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 )
98 1 2 81 77 96 64 97 dssmapfv3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
99 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 )
100 1 2 81 77 96 66 99 dssmapfv3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
101 98 100 uneq12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ∪ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) ) = ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
102 1 2 3 ntrclsfv1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐼 ) = 𝐾 )
103 102 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐷 ‘ 𝐼 ) = 𝐾 )
104 fveq1 ⊢ ( ( 𝐷 ‘ 𝐼 ) = 𝐾 → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐾 ‘ 𝑠 ) )
105 fveq1 ⊢ ( ( 𝐷 ‘ 𝐼 ) = 𝐾 → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) = ( 𝐾 ‘ 𝑡 ) )
106 104 105 uneq12d ⊢ ( ( 𝐷 ‘ 𝐼 ) = 𝐾 → ( ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ∪ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) )
107 103 106 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ∪ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑡 ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) )
108 101 107 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) )
109 108 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = 𝐵 ↔ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) = 𝐵 ) )
110 109 imbi2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∪ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) = 𝐵 ) ↔ ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) = 𝐵 ) ) )
111 95 110 bitrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) ) = ∅ → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ∅ ) ↔ ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) = 𝐵 ) ) )
112 61 62 63 111 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( ( ( 𝐵 ∖ 𝑠 ) ∩ ( 𝐵 ∖ 𝑡 ) ) = ∅ → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∩ ( 𝐼 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ∅ ) ↔ ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) = 𝐵 ) ) )
113 52 60 112 3bitrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = ( 𝐵 ∖ 𝑡 ) ) → ( ( ( 𝑎 ∩ 𝑏 ) = ∅ → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) ↔ ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) = 𝐵 ) ) )
114 32 44 113 ralxfrd2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = ( 𝐵 ∖ 𝑠 ) ) → ( ∀ 𝑏 ∈ 𝒫 𝐵 ( ( 𝑎 ∩ 𝑏 ) = ∅ → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) = 𝐵 ) ) )
115 18 29 114 ralxfrd2 ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝒫 𝐵 ∀ 𝑏 ∈ 𝒫 𝐵 ( ( 𝑎 ∩ 𝑏 ) = ∅ → ( ( 𝐼 ‘ 𝑎 ) ∩ ( 𝐼 ‘ 𝑏 ) ) = ∅ ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) = 𝐵 ) ) )
116 16 115 bitrid ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) = 𝐵 ) ) )