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

Theorem ntrclsk13 38686
 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 ↦ (𝑘 ∈ (𝒫 𝑖𝑚 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖𝑗))))))
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 3840 . . . . 5 (𝑠 = 𝑎 → (𝑠𝑡) = (𝑎𝑡))
21fveq2d 6233 . . . 4 (𝑠 = 𝑎 → (𝐼‘(𝑠𝑡)) = (𝐼‘(𝑎𝑡)))
3 fveq2 6229 . . . . 5 (𝑠 = 𝑎 → (𝐼𝑠) = (𝐼𝑎))
43ineq1d 3846 . . . 4 (𝑠 = 𝑎 → ((𝐼𝑠) ∩ (𝐼𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑡)))
52, 4eqeq12d 2666 . . 3 (𝑠 = 𝑎 → ((𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∩ (𝐼𝑡)) ↔ (𝐼‘(𝑎𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑡))))
6 ineq2 3841 . . . . 5 (𝑡 = 𝑏 → (𝑎𝑡) = (𝑎𝑏))
76fveq2d 6233 . . . 4 (𝑡 = 𝑏 → (𝐼‘(𝑎𝑡)) = (𝐼‘(𝑎𝑏)))
8 fveq2 6229 . . . . 5 (𝑡 = 𝑏 → (𝐼𝑡) = (𝐼𝑏))
98ineq2d 3847 . . . 4 (𝑡 = 𝑏 → ((𝐼𝑎) ∩ (𝐼𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑏)))
107, 9eqeq12d 2666 . . 3 (𝑡 = 𝑏 → ((𝐼‘(𝑎𝑡)) = ((𝐼𝑎) ∩ (𝐼𝑡)) ↔ (𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏))))
115, 10cbvral2v 3209 . 2 (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∩ (𝐼𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)))
12 ntrcls.d . . . . . 6 𝐷 = (𝑂𝐵)
13 ntrcls.r . . . . . 6 (𝜑𝐼𝐷𝐾)
1412, 13ntrclsbex 38649 . . . . 5 (𝜑𝐵 ∈ V)
15 difssd 3771 . . . . 5 (𝜑 → (𝐵𝑠) ⊆ 𝐵)
1614, 15sselpwd 4840 . . . 4 (𝜑 → (𝐵𝑠) ∈ 𝒫 𝐵)
1716adantr 480 . . 3 ((𝜑𝑠 ∈ 𝒫 𝐵) → (𝐵𝑠) ∈ 𝒫 𝐵)
18 elpwi 4201 . . . 4 (𝑎 ∈ 𝒫 𝐵𝑎𝐵)
1914adantr 480 . . . . . 6 ((𝜑𝑎𝐵) → 𝐵 ∈ V)
20 difssd 3771 . . . . . 6 ((𝜑𝑎𝐵) → (𝐵𝑎) ⊆ 𝐵)
2119, 20sselpwd 4840 . . . . 5 ((𝜑𝑎𝐵) → (𝐵𝑎) ∈ 𝒫 𝐵)
22 difeq2 3755 . . . . . . . 8 (𝑠 = (𝐵𝑎) → (𝐵𝑠) = (𝐵 ∖ (𝐵𝑎)))
2322eqeq2d 2661 . . . . . . 7 (𝑠 = (𝐵𝑎) → (𝑎 = (𝐵𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵𝑎))))
24 eqcom 2658 . . . . . . 7 (𝑎 = (𝐵 ∖ (𝐵𝑎)) ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎)
2523, 24syl6bb 276 . . . . . 6 (𝑠 = (𝐵𝑎) → (𝑎 = (𝐵𝑠) ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎))
2625adantl 481 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑠 = (𝐵𝑎)) → (𝑎 = (𝐵𝑠) ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎))
27 dfss4 3891 . . . . . . 7 (𝑎𝐵 ↔ (𝐵 ∖ (𝐵𝑎)) = 𝑎)
2827biimpi 206 . . . . . 6 (𝑎𝐵 → (𝐵 ∖ (𝐵𝑎)) = 𝑎)
2928adantl 481 . . . . 5 ((𝜑𝑎𝐵) → (𝐵 ∖ (𝐵𝑎)) = 𝑎)
3021, 26, 29rspcedvd 3348 . . . 4 ((𝜑𝑎𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠))
3118, 30sylan2 490 . . 3 ((𝜑𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠))
32 ineq1 3840 . . . . . . . 8 (𝑎 = (𝐵𝑠) → (𝑎𝑏) = ((𝐵𝑠) ∩ 𝑏))
3332fveq2d 6233 . . . . . . 7 (𝑎 = (𝐵𝑠) → (𝐼‘(𝑎𝑏)) = (𝐼‘((𝐵𝑠) ∩ 𝑏)))
34 fveq2 6229 . . . . . . . 8 (𝑎 = (𝐵𝑠) → (𝐼𝑎) = (𝐼‘(𝐵𝑠)))
3534ineq1d 3846 . . . . . . 7 (𝑎 = (𝐵𝑠) → ((𝐼𝑎) ∩ (𝐼𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)))
3633, 35eqeq12d 2666 . . . . . 6 (𝑎 = (𝐵𝑠) → ((𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ (𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏))))
3736ralbidv 3015 . . . . 5 (𝑎 = (𝐵𝑠) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏))))
38373ad2ant3 1104 . . . 4 ((𝜑𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏))))
39 difssd 3771 . . . . . . . 8 (𝜑 → (𝐵𝑡) ⊆ 𝐵)
4014, 39sselpwd 4840 . . . . . . 7 (𝜑 → (𝐵𝑡) ∈ 𝒫 𝐵)
4140ad2antrr 762 . . . . . 6 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵𝑡) ∈ 𝒫 𝐵)
42 simpll 805 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝜑)
43 elpwi 4201 . . . . . . . 8 (𝑏 ∈ 𝒫 𝐵𝑏𝐵)
4443adantl 481 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏𝐵)
45 difssd 3771 . . . . . . . . . 10 (𝜑 → (𝐵𝑏) ⊆ 𝐵)
4614, 45sselpwd 4840 . . . . . . . . 9 (𝜑 → (𝐵𝑏) ∈ 𝒫 𝐵)
4746adantr 480 . . . . . . . 8 ((𝜑𝑏𝐵) → (𝐵𝑏) ∈ 𝒫 𝐵)
48 difeq2 3755 . . . . . . . . . . 11 (𝑡 = (𝐵𝑏) → (𝐵𝑡) = (𝐵 ∖ (𝐵𝑏)))
4948eqeq2d 2661 . . . . . . . . . 10 (𝑡 = (𝐵𝑏) → (𝑏 = (𝐵𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵𝑏))))
50 eqcom 2658 . . . . . . . . . 10 (𝑏 = (𝐵 ∖ (𝐵𝑏)) ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5149, 50syl6bb 276 . . . . . . . . 9 (𝑡 = (𝐵𝑏) → (𝑏 = (𝐵𝑡) ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏))
5251adantl 481 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑡 = (𝐵𝑏)) → (𝑏 = (𝐵𝑡) ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏))
53 dfss4 3891 . . . . . . . . . 10 (𝑏𝐵 ↔ (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5453biimpi 206 . . . . . . . . 9 (𝑏𝐵 → (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5554adantl 481 . . . . . . . 8 ((𝜑𝑏𝐵) → (𝐵 ∖ (𝐵𝑏)) = 𝑏)
5647, 52, 55rspcedvd 3348 . . . . . . 7 ((𝜑𝑏𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡))
5742, 44, 56syl2anc 694 . . . . . 6 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡))
58 ineq2 3841 . . . . . . . . . . 11 (𝑏 = (𝐵𝑡) → ((𝐵𝑠) ∩ 𝑏) = ((𝐵𝑠) ∩ (𝐵𝑡)))
59 difundi 3912 . . . . . . . . . . 11 (𝐵 ∖ (𝑠𝑡)) = ((𝐵𝑠) ∩ (𝐵𝑡))
6058, 59syl6eqr 2703 . . . . . . . . . 10 (𝑏 = (𝐵𝑡) → ((𝐵𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠𝑡)))
6160fveq2d 6233 . . . . . . . . 9 (𝑏 = (𝐵𝑡) → (𝐼‘((𝐵𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠𝑡))))
62 fveq2 6229 . . . . . . . . . 10 (𝑏 = (𝐵𝑡) → (𝐼𝑏) = (𝐼‘(𝐵𝑡)))
6362ineq2d 3847 . . . . . . . . 9 (𝑏 = (𝐵𝑡) → ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))
6461, 63eqeq12d 2666 . . . . . . . 8 (𝑏 = (𝐵𝑡) → ((𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))))
65643ad2ant3 1104 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → ((𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))))
66 simp1l 1105 . . . . . . . . 9 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → 𝜑)
6766, 14jccir 561 . . . . . . . 8 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → (𝜑𝐵 ∈ V))
68 simp1r 1106 . . . . . . . 8 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → 𝑠 ∈ 𝒫 𝐵)
69 simp2 1082 . . . . . . . 8 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → 𝑡 ∈ 𝒫 𝐵)
70 ntrcls.o . . . . . . . . . . . . . 14 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖𝑚 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖𝑗))))))
7170, 12, 13ntrclsiex 38668 . . . . . . . . . . . . 13 (𝜑𝐼 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
72 elmapi 7921 . . . . . . . . . . . . 13 (𝐼 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
7371, 72syl 17 . . . . . . . . . . . 12 (𝜑𝐼:𝒫 𝐵⟶𝒫 𝐵)
7473anim1i 591 . . . . . . . . . . 11 ((𝜑𝐵 ∈ V) → (𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V))
7574adantr 480 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V))
76 simpl 472 . . . . . . . . . . . . 13 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
77 simpr 476 . . . . . . . . . . . . . 14 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → 𝐵 ∈ V)
78 difssd 3771 . . . . . . . . . . . . . 14 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵 ∖ (𝑠𝑡)) ⊆ 𝐵)
7977, 78sselpwd 4840 . . . . . . . . . . . . 13 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵 ∖ (𝑠𝑡)) ∈ 𝒫 𝐵)
8076, 79ffvelrnd 6400 . . . . . . . . . . . 12 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠𝑡))) ∈ 𝒫 𝐵)
8180elpwid 4203 . . . . . . . . . . 11 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠𝑡))) ⊆ 𝐵)
82 difssd 3771 . . . . . . . . . . . . . . 15 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵𝑠) ⊆ 𝐵)
8377, 82sselpwd 4840 . . . . . . . . . . . . . 14 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐵𝑠) ∈ 𝒫 𝐵)
8476, 83ffvelrnd 6400 . . . . . . . . . . . . 13 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵𝑠)) ∈ 𝒫 𝐵)
8584elpwid 4203 . . . . . . . . . . . 12 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → (𝐼‘(𝐵𝑠)) ⊆ 𝐵)
86 ssinss1 3874 . . . . . . . . . . . 12 ((𝐼‘(𝐵𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵)
8785, 86syl 17 . . . . . . . . . . 11 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵)
8881, 87jca 553 . . . . . . . . . 10 ((𝐼:𝒫 𝐵⟶𝒫 𝐵𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵))
89 rcompleq 38635 . . . . . . . . . 10 (((𝐼‘(𝐵 ∖ (𝑠𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))))
9075, 88, 893syl 18 . . . . . . . . 9 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))))
91 simplr 807 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
9271ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
93 eqid 2651 . . . . . . . . . . 11 (𝐷𝐼) = (𝐷𝐼)
94 simprl 809 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
9594elpwid 4203 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑠𝐵)
96 simprr 811 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
9796elpwid 4203 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝑡𝐵)
9895, 97unssd 3822 . . . . . . . . . . . 12 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (𝑠𝑡) ⊆ 𝐵)
9991, 98sselpwd 4840 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (𝑠𝑡) ∈ 𝒫 𝐵)
100 eqid 2651 . . . . . . . . . . 11 ((𝐷𝐼)‘(𝑠𝑡)) = ((𝐷𝐼)‘(𝑠𝑡))
10170, 12, 91, 92, 93, 99, 100dssmapfv3d 38630 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐷𝐼)‘(𝑠𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))))
102 simpl 472 . . . . . . . . . . . . 13 ((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
103 simplr 807 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
10471ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
105 simpr 476 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
106 eqid 2651 . . . . . . . . . . . . . 14 ((𝐷𝐼)‘𝑠) = ((𝐷𝐼)‘𝑠)
10770, 12, 103, 104, 93, 105, 106dssmapfv3d 38630 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → ((𝐷𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵𝑠))))
108102, 107sylan2 490 . . . . . . . . . . . 12 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐷𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵𝑠))))
109 simpr 476 . . . . . . . . . . . . 13 ((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
110 simplr 807 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
11171ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
112 simpr 476 . . . . . . . . . . . . . 14 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
113 eqid 2651 . . . . . . . . . . . . . 14 ((𝐷𝐼)‘𝑡) = ((𝐷𝐼)‘𝑡)
11470, 12, 110, 111, 93, 112, 113dssmapfv3d 38630 . . . . . . . . . . . . 13 (((𝜑𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵𝑡))))
115109, 114sylan2 490 . . . . . . . . . . . 12 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐷𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵𝑡))))
116108, 115uneq12d 3801 . . . . . . . . . . 11 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵𝑡)))))
117 difindi 3914 . . . . . . . . . . 11 (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵𝑡))))
118116, 117syl6eqr 2703 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡)))))
119101, 118eqeq12d 2666 . . . . . . . . 9 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘(𝑠𝑡)) = (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))))))
120 simpll 805 . . . . . . . . . 10 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → 𝜑)
12170, 12, 13ntrclsfv1 38670 . . . . . . . . . 10 (𝜑 → (𝐷𝐼) = 𝐾)
122 fveq1 6228 . . . . . . . . . . 11 ((𝐷𝐼) = 𝐾 → ((𝐷𝐼)‘(𝑠𝑡)) = (𝐾‘(𝑠𝑡)))
123 fveq1 6228 . . . . . . . . . . . 12 ((𝐷𝐼) = 𝐾 → ((𝐷𝐼)‘𝑠) = (𝐾𝑠))
124 fveq1 6228 . . . . . . . . . . . 12 ((𝐷𝐼) = 𝐾 → ((𝐷𝐼)‘𝑡) = (𝐾𝑡))
125123, 124uneq12d 3801 . . . . . . . . . . 11 ((𝐷𝐼) = 𝐾 → (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡)))
126122, 125eqeq12d 2666 . . . . . . . . . 10 ((𝐷𝐼) = 𝐾 → (((𝐷𝐼)‘(𝑠𝑡)) = (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
127120, 121, 1263syl 18 . . . . . . . . 9 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → (((𝐷𝐼)‘(𝑠𝑡)) = (((𝐷𝐼)‘𝑠) ∪ ((𝐷𝐼)‘𝑡)) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
12890, 119, 1273bitr2d 296 . . . . . . . 8 (((𝜑𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
12967, 68, 69, 128syl12anc 1364 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → ((𝐼‘(𝐵 ∖ (𝑠𝑡))) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼‘(𝐵𝑡))) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13065, 129bitrd 268 . . . . . 6 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵𝑡)) → ((𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ (𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13141, 57, 130ralxfrd2 4914 . . . . 5 ((𝜑𝑠 ∈ 𝒫 𝐵) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
1321313adant3 1101 . . . 4 ((𝜑𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵𝑠)) ∩ (𝐼𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13338, 132bitrd 268 . . 3 ((𝜑𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13417, 31, 133ralxfrd2 4914 . 2 (𝜑 → (∀𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎𝑏)) = ((𝐼𝑎) ∩ (𝐼𝑏)) ↔ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
13511, 134syl5bb 272 1 (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∩ (𝐼𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠𝑡)) = ((𝐾𝑠) ∪ (𝐾𝑡))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  𝒫 cpw 4191   class class class wbr 4685   ↦ cmpt 4762  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ↑𝑚 cmap 7899 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-map 7901 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator