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 44084
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 4213 . . . . 5 (𝑠 = 𝑎 → (𝑠𝑡) = (𝑎𝑡))
21fveq2d 6910 . . . 4 (𝑠 = 𝑎 → (𝐼‘(𝑠𝑡)) = (𝐼‘(𝑎𝑡)))
3 fveq2 6906 . . . . 5 (𝑠 = 𝑎 → (𝐼𝑠) = (𝐼𝑎))
43ineq1d 4219 . . . 4 (𝑠 = 𝑎 → ((𝐼𝑠) ∩ (𝐼𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑡)))
52, 4eqeq12d 2753 . . 3 (𝑠 = 𝑎 → ((𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∩ (𝐼𝑡)) ↔ (𝐼‘(𝑎𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑡))))
6 ineq2 4214 . . . . 5 (𝑡 = 𝑏 → (𝑎𝑡) = (𝑎𝑏))
76fveq2d 6910 . . . 4 (𝑡 = 𝑏 → (𝐼‘(𝑎𝑡)) = (𝐼‘(𝑎𝑏)))
8 fveq2 6906 . . . . 5 (𝑡 = 𝑏 → (𝐼𝑡) = (𝐼𝑏))
98ineq2d 4220 . . . 4 (𝑡 = 𝑏 → ((𝐼𝑎) ∩ (𝐼𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑏)))
107, 9eqeq12d 2753 . . 3 (𝑡 = 𝑏 → ((𝐼‘(𝑎𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑡)) ↔ (𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏))))
115, 10cbvral2vw 3241 . 2 (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∩ (𝐼𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)))
12 ntrcls.d . . . . . 6 𝐷 = (𝑂𝐵)
13 ntrcls.r . . . . . 6 (𝜑𝐼𝐷𝐾)
1412, 13ntrclsbex 44047 . . . . 5 (𝜑𝐵 ∈ V)
15 difssd 4137 . . . . 5 (𝜑 → (𝐵𝑠) ⊆ 𝐵)
1614, 15sselpwd 5328 . . . 4 (𝜑 → (𝐵𝑠) ∈ 𝒫 𝐵)
1716adantr 480 . . 3 ((𝜑𝑠 ∈ 𝒫 𝐵) → (𝐵𝑠) ∈ 𝒫 𝐵)
18 elpwi 4607 . . . 4 (𝑎 ∈ 𝒫 𝐵𝑎𝐵)
1914adantr 480 . . . . . 6 ((𝜑𝑎𝐵) → 𝐵 ∈ V)
20 difssd 4137 . . . . . 6 ((𝜑𝑎𝐵) → (𝐵𝑎) ⊆ 𝐵)
2119, 20sselpwd 5328 . . . . 5 ((𝜑𝑎𝐵) → (𝐵𝑎) ∈ 𝒫 𝐵)
22 difeq2 4120 . . . . . . . 8 (𝑠 = (𝐵𝑎) → (𝐵𝑠) = (𝐵 ∖ (𝐵𝑎)))
2322eqeq2d 2748 . . . . . . 7 (𝑠 = (𝐵𝑎) → (𝑎 = (𝐵𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵𝑎))))
24 eqcom 2744 . . . . . . 7 (𝑎 = (𝐵 ∖ (𝐵𝑎)) ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎)
2523, 24bitrdi 287 . . . . . 6 (𝑠 = (𝐵𝑎) → (𝑎 = (𝐵𝑠) ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎))
2625adantl 481 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑠 = (𝐵𝑎)) → (𝑎 = (𝐵𝑠) ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎))
27 dfss4 4269 . . . . . . 7 (𝑎𝐵 ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎)
2827biimpi 216 . . . . . 6 (𝑎𝐵 → (𝐵 ∖ (𝐵𝑎)) = 𝑎)
2928adantl 481 . . . . 5 ((𝜑𝑎𝐵) → (𝐵 ∖ (𝐵𝑎)) = 𝑎)
3021, 26, 29rspcedvd 3624 . . . 4 ((𝜑𝑎𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠))
3118, 30sylan2 593 . . 3 ((𝜑𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠))
32 ineq1 4213 . . . . . . . 8 (𝑎 = (𝐵𝑠) → (𝑎𝑏) = ((𝐵𝑠) ∩ 𝑏))
3332fveq2d 6910 . . . . . . 7 (𝑎 = (𝐵𝑠) → (𝐼‘(𝑎𝑏)) = (𝐼‘((𝐵𝑠) ∩ 𝑏)))
34 fveq2 6906 . . . . . . . 8 (𝑎 = (𝐵𝑠) → (𝐼𝑎) = (𝐼‘(𝐵𝑠)))
3534ineq1d 4219 . . . . . . 7 (𝑎 = (𝐵𝑠) → ((𝐼𝑎) ∩ (𝐼𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)))
3633, 35eqeq12d 2753 . . . . . 6 (𝑎 = (𝐵𝑠) → ((𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ (𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏))))
3736ralbidv 3178 . . . . 5 (𝑎 = (𝐵𝑠) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏))))
38373ad2ant3 1136 . . . 4 ((𝜑𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏))))
39 difssd 4137 . . . . . . . 8 (𝜑 → (𝐵𝑡) ⊆ 𝐵)
4014, 39sselpwd 5328 . . . . . . 7 (𝜑 → (𝐵𝑡) ∈ 𝒫 𝐵)
4140ad2antrr 726 . . . . . 6 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵𝑡) ∈ 𝒫 𝐵)
42 simpll 767 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝜑)
43 elpwi 4607 . . . . . . . 8 (𝑏 ∈ 𝒫 𝐵𝑏𝐵)
4443adantl 481 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏𝐵)
45 difssd 4137 . . . . . . . . . 10 (𝜑 → (𝐵𝑏) ⊆ 𝐵)
4614, 45sselpwd 5328 . . . . . . . . 9 (𝜑 → (𝐵𝑏) ∈ 𝒫 𝐵)
4746adantr 480 . . . . . . . 8 ((𝜑𝑏𝐵) → (𝐵𝑏) ∈ 𝒫 𝐵)
48 difeq2 4120 . . . . . . . . . . 11 (𝑡 = (𝐵𝑏) → (𝐵𝑡) = (𝐵 ∖ (𝐵𝑏)))
4948eqeq2d 2748 . . . . . . . . . 10 (𝑡 = (𝐵𝑏) → (𝑏 = (𝐵𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵𝑏))))
50 eqcom 2744 . . . . . . . . . 10 (𝑏 = (𝐵 ∖ (𝐵𝑏)) ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5149, 50bitrdi 287 . . . . . . . . 9 (𝑡 = (𝐵𝑏) → (𝑏 = (𝐵𝑡) ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏))
5251adantl 481 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑡 = (𝐵𝑏)) → (𝑏 = (𝐵𝑡) ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏))
53 dfss4 4269 . . . . . . . . . 10 (𝑏𝐵 ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5453biimpi 216 . . . . . . . . 9 (𝑏𝐵 → (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5554adantl 481 . . . . . . . 8 ((𝜑𝑏𝐵) → (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5647, 52, 55rspcedvd 3624 . . . . . . 7 ((𝜑𝑏𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡))
5742, 44, 56syl2anc 584 . . . . . 6 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡))
58 ineq2 4214 . . . . . . . . . . 11 (𝑏 = (𝐵𝑡) → ((𝐵𝑠) ∩ 𝑏) = ((𝐵𝑠) ∩ (𝐵𝑡)))
59 difundi 4290 . . . . . . . . . . 11 (𝐵 ∖ (𝑠𝑡)) = ((𝐵𝑠) ∩ (𝐵𝑡))
6058, 59eqtr4di 2795 . . . . . . . . . 10 (𝑏 = (𝐵𝑡) → ((𝐵𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠𝑡)))
6160fveq2d 6910 . . . . . . . . 9 (𝑏 = (𝐵𝑡) → (𝐼‘((𝐵𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠𝑡))))
62 fveq2 6906 . . . . . . . . . 10 (𝑏 = (𝐵𝑡) → (𝐼𝑏) = (𝐼‘(𝐵𝑡)))
6362ineq2d 4220 . . . . . . . . 9 (𝑏 = (𝐵𝑡) → ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))
6461, 63eqeq12d 2753 . . . . . . . 8 (𝑏 = (𝐵𝑡) → ((𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))))
65643ad2ant3 1136 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → ((𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))))
66 simp1l 1198 . . . . . . . . 9 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → 𝜑)
6766, 14jccir 521 . . . . . . . 8 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → (𝜑𝐵 ∈ V))
68 simp1r 1199 . . . . . . . 8 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → 𝑠 ∈ 𝒫 𝐵)
69 simp2 1138 . . . . . . . 8 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → 𝑡 ∈ 𝒫 𝐵)
70 ntrcls.o . . . . . . . . . . . . . 14 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖𝑗))))))
7170, 12, 13ntrclsiex 44066 . . . . . . . . . . . . 13 (𝜑𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵))
72 elmapi 8889 . . . . . . . . . . . . 13 (𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
7371, 72syl 17 . . . . . . . . . . . 12 (𝜑𝐼:𝒫 𝐵⟶𝒫 𝐵)
7473anim1i 615 . . . . . . . . . . 11 ((𝜑𝐵 ∈ V) → (𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V))
7574adantr 480 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V))
76 simpl 482 . . . . . . . . . . . . 13 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
77 simpr 484 . . . . . . . . . . . . . 14 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → 𝐵 ∈ V)
78 difssd 4137 . . . . . . . . . . . . . 14 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵 ∖ (𝑠𝑡)) ⊆ 𝐵)
7977, 78sselpwd 5328 . . . . . . . . . . . . 13 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵 ∖ (𝑠𝑡)) ∈ 𝒫 𝐵)
8076, 79ffvelcdmd 7105 . . . . . . . . . . . 12 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠𝑡))) ∈ 𝒫 𝐵)
8180elpwid 4609 . . . . . . . . . . 11 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠𝑡))) ⊆ 𝐵)
82 difssd 4137 . . . . . . . . . . . . . . 15 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵𝑠) ⊆ 𝐵)
8377, 82sselpwd 5328 . . . . . . . . . . . . . 14 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵𝑠) ∈ 𝒫 𝐵)
8476, 83ffvelcdmd 7105 . . . . . . . . . . . . 13 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵𝑠)) ∈ 𝒫 𝐵)
8584elpwid 4609 . . . . . . . . . . . 12 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵𝑠)) ⊆ 𝐵)
86 ssinss1 4246 . . . . . . . . . . . 12 ((𝐼‘(𝐵𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵)
8785, 86syl 17 . . . . . . . . . . 11 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵)
8881, 87jca 511 . . . . . . . . . 10 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵))
89 rcompleq 4305 . . . . . . . . . 10 (((𝐼‘(𝐵 ∖ (𝑠𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))))
9075, 88, 893syl 18 . . . . . . . . 9 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))))
91 simplr 769 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
9271ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵))
93 eqid 2737 . . . . . . . . . . 11 (𝐷𝐼) = (𝐷𝐼)
94 simprl 771 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
9594elpwid 4609 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑠𝐵)
96 simprr 773 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
9796elpwid 4609 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑡𝐵)
9895, 97unssd 4192 . . . . . . . . . . . 12 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (𝑠𝑡) ⊆ 𝐵)
9991, 98sselpwd 5328 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (𝑠𝑡) ∈ 𝒫 𝐵)
100 eqid 2737 . . . . . . . . . . 11 ((𝐷𝐼)‘(𝑠𝑡)) = ((𝐷𝐼)‘(𝑠𝑡))
10170, 12, 91, 92, 93, 99, 100dssmapfv3d 44032 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐷𝐼)‘(𝑠𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))))
102 simpl 482 . . . . . . . . . . . . 13 ((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
103 simplr 769 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
10471ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵))
105 simpr 484 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
106 eqid 2737 . . . . . . . . . . . . . 14 ((𝐷𝐼)‘𝑠) = ((𝐷𝐼)‘𝑠)
10770, 12, 103, 104, 93, 105, 106dssmapfv3d 44032 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → ((𝐷𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵𝑠))))
108102, 107sylan2 593 . . . . . . . . . . . 12 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐷𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵𝑠))))
109 simpr 484 . . . . . . . . . . . . 13 ((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
110 simplr 769 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
11171ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵m 𝒫 𝐵))
112 simpr 484 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
113 eqid 2737 . . . . . . . . . . . . . 14 ((𝐷𝐼)‘𝑡) = ((𝐷𝐼)‘𝑡)
11470, 12, 110, 111, 93, 112, 113dssmapfv3d 44032 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵𝑡))))
115109, 114sylan2 593 . . . . . . . . . . . 12 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐷𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵𝑡))))
116108, 115uneq12d 4169 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵𝑡)))))
117 difindi 4292 . . . . . . . . . . 11 (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵𝑡))))
118116, 117eqtr4di 2795 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))))
119101, 118eqeq12d 2753 . . . . . . . . 9 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘(𝑠𝑡)) = (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))))
120 simpll 767 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝜑)
12170, 12, 13ntrclsfv1 44068 . . . . . . . . . 10 (𝜑 → (𝐷𝐼) = 𝐾)
122 fveq1 6905 . . . . . . . . . . 11 ((𝐷𝐼) = 𝐾 → ((𝐷𝐼)‘(𝑠𝑡)) = (𝐾‘(𝑠𝑡)))
123 fveq1 6905 . . . . . . . . . . . 12 ((𝐷𝐼) = 𝐾 → ((𝐷𝐼)‘𝑠) = (𝐾𝑠))
124 fveq1 6905 . . . . . . . . . . . 12 ((𝐷𝐼) = 𝐾 → ((𝐷𝐼)‘𝑡) = (𝐾𝑡))
125123, 124uneq12d 4169 . . . . . . . . . . 11 ((𝐷𝐼) = 𝐾 → (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡)))
126122, 125eqeq12d 2753 . . . . . . . . . 10 ((𝐷𝐼) = 𝐾 → (((𝐷𝐼)‘(𝑠𝑡)) = (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
127120, 121, 1263syl 18 . . . . . . . . 9 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘(𝑠𝑡)) = (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
12890, 119, 1273bitr2d 307 . . . . . . . 8 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
12967, 68, 69, 128syl12anc 837 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13065, 129bitrd 279 . . . . . 6 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → ((𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13141, 57, 130ralxfrd2 5412 . . . . 5 ((𝜑𝑠 ∈ 𝒫 𝐵) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
1321313adant3 1133 . . . 4 ((𝜑𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13338, 132bitrd 279 . . 3 ((𝜑𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13417, 31, 133ralxfrd2 5412 . 2 (𝜑 → (∀𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13511, 134bitrid 283 1 (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∩ (𝐼𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  Vcvv 3480  cdif 3948  cun 3949  cin 3950  wss 3951  𝒫 cpw 4600   class class class wbr 5143  cmpt 5225  wf 6557  cfv 6561  (class class class)co 7431  m cmap 8866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-map 8868
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator