Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ntrclsk13 Structured version   Visualization version   GIF version

Theorem ntrclsk13 41663
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.)
Hypotheses
Ref Expression
ntrcls.o 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖𝑗))))))
ntrcls.d 𝐷 = (𝑂𝐵)
ntrcls.r (𝜑𝐼𝐷𝐾)
Assertion
Ref Expression
ntrclsk13 (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∩ (𝐼𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
Distinct variable groups:   𝐵,𝑠,𝑡,𝑖,𝑗,𝑘   𝐼,𝑠,𝑡,𝑖,𝑗,𝑘   𝜑,𝑠,𝑡,𝑖,𝑗,𝑘
Allowed substitution hints:   𝐷(𝑡,𝑖,𝑗,𝑘,𝑠)   𝐾(𝑡,𝑖,𝑗,𝑘,𝑠)   𝑂(𝑡,𝑖,𝑗,𝑘,𝑠)

Proof of Theorem ntrclsk13
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ineq1 4145 . . . . 5 (𝑠 = 𝑎 → (𝑠𝑡) = (𝑎𝑡))
21fveq2d 6775 . . . 4 (𝑠 = 𝑎 → (𝐼‘(𝑠𝑡)) = (𝐼‘(𝑎𝑡)))
3 fveq2 6771 . . . . 5 (𝑠 = 𝑎 → (𝐼𝑠) = (𝐼𝑎))
43ineq1d 4151 . . . 4 (𝑠 = 𝑎 → ((𝐼𝑠) ∩ (𝐼𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑡)))
52, 4eqeq12d 2756 . . 3 (𝑠 = 𝑎 → ((𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∩ (𝐼𝑡)) ↔ (𝐼‘(𝑎𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑡))))
6 ineq2 4146 . . . . 5 (𝑡 = 𝑏 → (𝑎𝑡) = (𝑎𝑏))
76fveq2d 6775 . . . 4 (𝑡 = 𝑏 → (𝐼‘(𝑎𝑡)) = (𝐼‘(𝑎𝑏)))
8 fveq2 6771 . . . . 5 (𝑡 = 𝑏 → (𝐼𝑡) = (𝐼𝑏))
98ineq2d 4152 . . . 4 (𝑡 = 𝑏 → ((𝐼𝑎) ∩ (𝐼𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑏)))
107, 9eqeq12d 2756 . . 3 (𝑡 = 𝑏 → ((𝐼‘(𝑎𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑡)) ↔ (𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏))))
115, 10cbvral2vw 3394 . 2 (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∩ (𝐼𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)))
12 ntrcls.d . . . . . 6 𝐷 = (𝑂𝐵)
13 ntrcls.r . . . . . 6 (𝜑𝐼𝐷𝐾)
1412, 13ntrclsbex 41626 . . . . 5 (𝜑𝐵 ∈ V)
15 difssd 4072 . . . . 5 (𝜑 → (𝐵𝑠) ⊆ 𝐵)
1614, 15sselpwd 5254 . . . 4 (𝜑 → (𝐵𝑠) ∈ 𝒫 𝐵)
1716adantr 481 . . 3 ((𝜑𝑠 ∈ 𝒫 𝐵) → (𝐵𝑠) ∈ 𝒫 𝐵)
18 elpwi 4548 . . . 4 (𝑎 ∈ 𝒫 𝐵𝑎𝐵)
1914adantr 481 . . . . . 6 ((𝜑𝑎𝐵) → 𝐵 ∈ V)
20 difssd 4072 . . . . . 6 ((𝜑𝑎𝐵) → (𝐵𝑎) ⊆ 𝐵)
2119, 20sselpwd 5254 . . . . 5 ((𝜑𝑎𝐵) → (𝐵𝑎) ∈ 𝒫 𝐵)
22 difeq2 4056 . . . . . . . 8 (𝑠 = (𝐵𝑎) → (𝐵𝑠) = (𝐵 ∖ (𝐵𝑎)))
2322eqeq2d 2751 . . . . . . 7 (𝑠 = (𝐵𝑎) → (𝑎 = (𝐵𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵𝑎))))
24 eqcom 2747 . . . . . . 7 (𝑎 = (𝐵 ∖ (𝐵𝑎)) ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎)
2523, 24bitrdi 287 . . . . . 6 (𝑠 = (𝐵𝑎) → (𝑎 = (𝐵𝑠) ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎))
2625adantl 482 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑠 = (𝐵𝑎)) → (𝑎 = (𝐵𝑠) ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎))
27 dfss4 4198 . . . . . . 7 (𝑎𝐵 ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎)
2827biimpi 215 . . . . . 6 (𝑎𝐵 → (𝐵 ∖ (𝐵𝑎)) = 𝑎)
2928adantl 482 . . . . 5 ((𝜑𝑎𝐵) → (𝐵 ∖ (𝐵𝑎)) = 𝑎)
3021, 26, 29rspcedvd 3564 . . . 4 ((𝜑𝑎𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠))
3118, 30sylan2 593 . . 3 ((𝜑𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠))
32 ineq1 4145 . . . . . . . 8 (𝑎 = (𝐵𝑠) → (𝑎𝑏) = ((𝐵𝑠) ∩ 𝑏))
3332fveq2d 6775 . . . . . . 7 (𝑎 = (𝐵𝑠) → (𝐼‘(𝑎𝑏)) = (𝐼‘((𝐵𝑠) ∩ 𝑏)))
34 fveq2 6771 . . . . . . . 8 (𝑎 = (𝐵𝑠) → (𝐼𝑎) = (𝐼‘(𝐵𝑠)))
3534ineq1d 4151 . . . . . . 7 (𝑎 = (𝐵𝑠) → ((𝐼𝑎) ∩ (𝐼𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)))
3633, 35eqeq12d 2756 . . . . . 6 (𝑎 = (𝐵𝑠) → ((𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ (𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏))))
3736ralbidv 3123 . . . . 5 (𝑎 = (𝐵𝑠) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏))))
38373ad2ant3 1134 . . . 4 ((𝜑𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏))))
39 difssd 4072 . . . . . . . 8 (𝜑 → (𝐵𝑡) ⊆ 𝐵)
4014, 39sselpwd 5254 . . . . . . 7 (𝜑 → (𝐵𝑡) ∈ 𝒫 𝐵)
4140ad2antrr 723 . . . . . 6 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵𝑡) ∈ 𝒫 𝐵)
42 simpll 764 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝜑)
43 elpwi 4548 . . . . . . . 8 (𝑏 ∈ 𝒫 𝐵𝑏𝐵)
4443adantl 482 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏𝐵)
45 difssd 4072 . . . . . . . . . 10 (𝜑 → (𝐵𝑏) ⊆ 𝐵)
4614, 45sselpwd 5254 . . . . . . . . 9 (𝜑 → (𝐵𝑏) ∈ 𝒫 𝐵)
4746adantr 481 . . . . . . . 8 ((𝜑𝑏𝐵) → (𝐵𝑏) ∈ 𝒫 𝐵)
48 difeq2 4056 . . . . . . . . . . 11 (𝑡 = (𝐵𝑏) → (𝐵𝑡) = (𝐵 ∖ (𝐵𝑏)))
4948eqeq2d 2751 . . . . . . . . . 10 (𝑡 = (𝐵𝑏) → (𝑏 = (𝐵𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵𝑏))))
50 eqcom 2747 . . . . . . . . . 10 (𝑏 = (𝐵 ∖ (𝐵𝑏)) ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5149, 50bitrdi 287 . . . . . . . . 9 (𝑡 = (𝐵𝑏) → (𝑏 = (𝐵𝑡) ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏))
5251adantl 482 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑡 = (𝐵𝑏)) → (𝑏 = (𝐵𝑡) ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏))
53 dfss4 4198 . . . . . . . . . 10 (𝑏𝐵 ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5453biimpi 215 . . . . . . . . 9 (𝑏𝐵 → (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5554adantl 482 . . . . . . . 8 ((𝜑𝑏𝐵) → (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5647, 52, 55rspcedvd 3564 . . . . . . 7 ((𝜑𝑏𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡))
5742, 44, 56syl2anc 584 . . . . . 6 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡))
58 ineq2 4146 . . . . . . . . . . 11 (𝑏 = (𝐵𝑡) → ((𝐵𝑠) ∩ 𝑏) = ((𝐵𝑠) ∩ (𝐵𝑡)))
59 difundi 4219 . . . . . . . . . . 11 (𝐵 ∖ (𝑠𝑡)) = ((𝐵𝑠) ∩ (𝐵𝑡))
6058, 59eqtr4di 2798 . . . . . . . . . 10 (𝑏 = (𝐵𝑡) → ((𝐵𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠𝑡)))
6160fveq2d 6775 . . . . . . . . 9 (𝑏 = (𝐵𝑡) → (𝐼‘((𝐵𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠𝑡))))
62 fveq2 6771 . . . . . . . . . 10 (𝑏 = (𝐵𝑡) → (𝐼𝑏) = (𝐼‘(𝐵𝑡)))
6362ineq2d 4152 . . . . . . . . 9 (𝑏 = (𝐵𝑡) → ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))
6461, 63eqeq12d 2756 . . . . . . . 8 (𝑏 = (𝐵𝑡) → ((𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))))
65643ad2ant3 1134 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → ((𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))))
66 simp1l 1196 . . . . . . . . 9 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → 𝜑)
6766, 14jccir 522 . . . . . . . 8 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → (𝜑𝐵 ∈ V))
68 simp1r 1197 . . . . . . . 8 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → 𝑠 ∈ 𝒫 𝐵)
69 simp2 1136 . . . . . . . 8 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → 𝑡 ∈ 𝒫 𝐵)
70 ntrcls.o . . . . . . . . . . . . . 14 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖𝑗))))))
7170, 12, 13ntrclsiex 41645 . . . . . . . . . . . . 13 (𝜑𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵))
72 elmapi 8629 . . . . . . . . . . . . 13 (𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
7371, 72syl 17 . . . . . . . . . . . 12 (𝜑𝐼:𝒫 𝐵⟶𝒫 𝐵)
7473anim1i 615 . . . . . . . . . . 11 ((𝜑𝐵 ∈ V) → (𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V))
7574adantr 481 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V))
76 simpl 483 . . . . . . . . . . . . 13 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
77 simpr 485 . . . . . . . . . . . . . 14 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → 𝐵 ∈ V)
78 difssd 4072 . . . . . . . . . . . . . 14 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵 ∖ (𝑠𝑡)) ⊆ 𝐵)
7977, 78sselpwd 5254 . . . . . . . . . . . . 13 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵 ∖ (𝑠𝑡)) ∈ 𝒫 𝐵)
8076, 79ffvelrnd 6959 . . . . . . . . . . . 12 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠𝑡))) ∈ 𝒫 𝐵)
8180elpwid 4550 . . . . . . . . . . 11 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠𝑡))) ⊆ 𝐵)
82 difssd 4072 . . . . . . . . . . . . . . 15 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵𝑠) ⊆ 𝐵)
8377, 82sselpwd 5254 . . . . . . . . . . . . . 14 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵𝑠) ∈ 𝒫 𝐵)
8476, 83ffvelrnd 6959 . . . . . . . . . . . . 13 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵𝑠)) ∈ 𝒫 𝐵)
8584elpwid 4550 . . . . . . . . . . . 12 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵𝑠)) ⊆ 𝐵)
86 ssinss1 4177 . . . . . . . . . . . 12 ((𝐼‘(𝐵𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵)
8785, 86syl 17 . . . . . . . . . . 11 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵)
8881, 87jca 512 . . . . . . . . . 10 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵))
89 rcompleq 4235 . . . . . . . . . 10 (((𝐼‘(𝐵 ∖ (𝑠𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))))
9075, 88, 893syl 18 . . . . . . . . 9 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))))
91 simplr 766 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
9271ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵))
93 eqid 2740 . . . . . . . . . . 11 (𝐷𝐼) = (𝐷𝐼)
94 simprl 768 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
9594elpwid 4550 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑠𝐵)
96 simprr 770 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
9796elpwid 4550 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑡𝐵)
9895, 97unssd 4125 . . . . . . . . . . . 12 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (𝑠𝑡) ⊆ 𝐵)
9991, 98sselpwd 5254 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (𝑠𝑡) ∈ 𝒫 𝐵)
100 eqid 2740 . . . . . . . . . . 11 ((𝐷𝐼)‘(𝑠𝑡)) = ((𝐷𝐼)‘(𝑠𝑡))
10170, 12, 91, 92, 93, 99, 100dssmapfv3d 41609 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐷𝐼)‘(𝑠𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))))
102 simpl 483 . . . . . . . . . . . . 13 ((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
103 simplr 766 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
10471ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵))
105 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
106 eqid 2740 . . . . . . . . . . . . . 14 ((𝐷𝐼)‘𝑠) = ((𝐷𝐼)‘𝑠)
10770, 12, 103, 104, 93, 105, 106dssmapfv3d 41609 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → ((𝐷𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵𝑠))))
108102, 107sylan2 593 . . . . . . . . . . . 12 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐷𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵𝑠))))
109 simpr 485 . . . . . . . . . . . . 13 ((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
110 simplr 766 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
11171ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵))
112 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
113 eqid 2740 . . . . . . . . . . . . . 14 ((𝐷𝐼)‘𝑡) = ((𝐷𝐼)‘𝑡)
11470, 12, 110, 111, 93, 112, 113dssmapfv3d 41609 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵𝑡))))
115109, 114sylan2 593 . . . . . . . . . . . 12 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐷𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵𝑡))))
116108, 115uneq12d 4103 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵𝑡)))))
117 difindi 4221 . . . . . . . . . . 11 (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵𝑡))))
118116, 117eqtr4di 2798 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))))
119101, 118eqeq12d 2756 . . . . . . . . 9 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘(𝑠𝑡)) = (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))))
120 simpll 764 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝜑)
12170, 12, 13ntrclsfv1 41647 . . . . . . . . . 10 (𝜑 → (𝐷𝐼) = 𝐾)
122 fveq1 6770 . . . . . . . . . . 11 ((𝐷𝐼) = 𝐾 → ((𝐷𝐼)‘(𝑠𝑡)) = (𝐾‘(𝑠𝑡)))
123 fveq1 6770 . . . . . . . . . . . 12 ((𝐷𝐼) = 𝐾 → ((𝐷𝐼)‘𝑠) = (𝐾𝑠))
124 fveq1 6770 . . . . . . . . . . . 12 ((𝐷𝐼) = 𝐾 → ((𝐷𝐼)‘𝑡) = (𝐾𝑡))
125123, 124uneq12d 4103 . . . . . . . . . . 11 ((𝐷𝐼) = 𝐾 → (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡)))
126122, 125eqeq12d 2756 . . . . . . . . . 10 ((𝐷𝐼) = 𝐾 → (((𝐷𝐼)‘(𝑠𝑡)) = (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
127120, 121, 1263syl 18 . . . . . . . . 9 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘(𝑠𝑡)) = (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
12890, 119, 1273bitr2d 307 . . . . . . . 8 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
12967, 68, 69, 128syl12anc 834 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13065, 129bitrd 278 . . . . . 6 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → ((𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13141, 57, 130ralxfrd2 5339 . . . . 5 ((𝜑𝑠 ∈ 𝒫 𝐵) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
1321313adant3 1131 . . . 4 ((𝜑𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13338, 132bitrd 278 . . 3 ((𝜑𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13417, 31, 133ralxfrd2 5339 . 2 (𝜑 → (∀𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13511, 134syl5bb 283 1 (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∩ (𝐼𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1542  wcel 2110  wral 3066  wrex 3067  Vcvv 3431  cdif 3889  cun 3890  cin 3891  wss 3892  𝒫 cpw 4539   class class class wbr 5079  cmpt 5162  wf 6428  cfv 6432  (class class class)co 7272  m cmap 8607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7583
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7275  df-oprab 7276  df-mpo 7277  df-1st 7825  df-2nd 7826  df-map 8609
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator