ntrclskb - Mathbox for Richard Penner

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

Theorem ntrclskb 39917

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.)

**Hypotheses**
Ref	Expression
ntrcls.o	⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_𝑚 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
ntrcls.d	⊢ 𝐷 = (𝑂‘𝐵)
ntrcls.r	⊢ (𝜑 → 𝐼𝐷𝐾)

**Assertion**
Ref	Expression
ntrclskb	⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))

Distinct variable groups: 𝐵,𝑠,𝑡,𝑖,𝑗,𝑘 𝐼,𝑠,𝑡,𝑗,𝑘 𝜑,𝑠,𝑡,𝑖,𝑗,𝑘 Allowed substitution hints: 𝐷(𝑡,𝑖,𝑗,𝑘,𝑠) 𝐼(𝑖) 𝐾(𝑡,𝑖,𝑗,𝑘,𝑠) 𝑂(𝑡,𝑖,𝑗,𝑘,𝑠)

Proof of Theorem ntrclskb Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ineq1 4103	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
2	1	eqeq1d 2796	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝑠 ∩ 𝑡) = ∅ ↔ (𝑎 ∩ 𝑡) = ∅))
3		fveq2 6541	. . . . . 6 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
4	3	ineq1d 4110	. . . . 5 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
5	4	eqeq1d 2796	. . . 4 ⊢ (𝑠 = 𝑎 → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅))
6	2, 5	imbi12d 346	. . 3 ⊢ (𝑠 = 𝑎 → (((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝑎 ∩ 𝑡) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅)))
7		ineq2 4105	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
8	7	eqeq1d 2796	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝑎 ∩ 𝑡) = ∅ ↔ (𝑎 ∩ 𝑏) = ∅))
9		fveq2 6541	. . . . . 6 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
10	9	ineq2d 4111	. . . . 5 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
11	10	eqeq1d 2796	. . . 4 ⊢ (𝑡 = 𝑏 → (((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅))
12	8, 11	imbi12d 346	. . 3 ⊢ (𝑡 = 𝑏 → (((𝑎 ∩ 𝑡) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅)))
13	6, 12	cbvral2v 3411	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅))
14		ntrcls.d	. . . . 5 ⊢ 𝐷 = (𝑂‘𝐵)
15		ntrcls.r	. . . . 5 ⊢ (𝜑 → 𝐼𝐷𝐾)
16	14, 15	ntrclsrcomplex 39883	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18	14, 15	ntrclsrcomplex 39883	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
19	18	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
20		difeq2 4016	. . . . . 6 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
21	20	eqeq2d 2804	. . . . 5 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
22	21	adantl 482	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
23		elpwi 4465	. . . . . . 7 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
24		dfss4 4157	. . . . . . 7 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
25	23, 24	sylib 219	. . . . . 6 ⊢ (𝑎 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
26	25	eqcomd 2800	. . . . 5 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))
27	26	adantl 482	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))
28	19, 22, 27	rspcedvd 3564	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
29		simpl1 1184	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝜑)
30	14, 15	ntrclsrcomplex 39883	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
31	29, 30	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
32	14, 15	ntrclsrcomplex 39883	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
33	32	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
34		difeq2 4016	. . . . . . . 8 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
35	34	eqeq2d 2804	. . . . . . 7 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
36	35	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
37		elpwi 4465	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
38		dfss4 4157	. . . . . . . . 9 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
39	37, 38	sylib 219	. . . . . . . 8 ⊢ (𝑏 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
40	39	eqcomd 2800	. . . . . . 7 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))
41	40	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))
42	33, 36, 41	rspcedvd 3564	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
43	42	3ad2antl1 1178	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
44		simp13 1198	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑎 = (𝐵 ∖ 𝑠))
45		ineq1 4103	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
46	45	eqeq1d 2796	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝑎 ∩ 𝑏) = ∅ ↔ ((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅))
47		fveq2 6541	. . . . . . . . 9 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
48	47	ineq1d 4110	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
49	48	eqeq1d 2796	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅ ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅))
50	46, 49	imbi12d 346	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅)))
51	44, 50	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅)))
52		simp3 1131	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑏 = (𝐵 ∖ 𝑡))
53		ineq2 4105	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
54	53	eqeq1d 2796	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ ↔ ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅))
55		fveq2 6541	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
56	55	ineq2d 4111	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
57	56	eqeq1d 2796	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅ ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅))
58	54, 57	imbi12d 346	. . . . . 6 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅)))
59	52, 58	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅)))
60		simp11 1196	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
61		simp12 1197	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
62		simp2 1130	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
63		simp2 1130	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
64	63	elpwid 4467	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ⊆ 𝐵)
65		simp3 1131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
66	65	elpwid 4467	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ⊆ 𝐵)
67	64, 66	unssd 4085	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
68		ssid 3912	. . . . . . . . . 10 ⊢ 𝐵 ⊆ 𝐵
69		rcompleq 39868	. . . . . . . . . 10 ⊢ (((𝑠 ∪ 𝑡) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵) → ((𝑠 ∪ 𝑡) = 𝐵 ↔ (𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵)))
70	67, 68, 69	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∪ 𝑡) = 𝐵 ↔ (𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵)))
71		difundi 4178	. . . . . . . . . 10 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
72		difid 4252	. . . . . . . . . 10 ⊢ (𝐵 ∖ 𝐵) = ∅
73	71, 72	eqeq12i 2808	. . . . . . . . 9 ⊢ ((𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵) ↔ ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅)
74	70, 73	syl6rbb 289	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ ↔ (𝑠 ∪ 𝑡) = 𝐵))
75		ntrcls.o	. . . . . . . . . . . . . . . 16 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_𝑚 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
76	75, 14, 15	ntrclsiex 39901	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵))
77	76	3ad2ant1 1126	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵))
78		elmapi 8281	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
79	77, 78	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
80	14, 15	ntrclsbex 39882	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ V)
81	80	3ad2ant1 1126	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
82		difssd 4032	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
83	81, 82	sselpwd 5124	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
84	79, 83	ffvelrnd 6720	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
85	84	elpwid 4467	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
86		ssinss1 4136	. . . . . . . . . . 11 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
87	85, 86	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
88		0ss 4272	. . . . . . . . . 10 ⊢ ∅ ⊆ 𝐵
89		rcompleq 39868	. . . . . . . . . 10 ⊢ ((((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ ∅ ⊆ 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅)))
90	87, 88, 89	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅)))
91		difindi 4180	. . . . . . . . . 10 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
92		dif0 4254	. . . . . . . . . 10 ⊢ (𝐵 ∖ ∅) = 𝐵
93	91, 92	eqeq12i 2808	. . . . . . . . 9 ⊢ ((𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅) ↔ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵)
94	90, 93	syl6bb 288	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵))
95	74, 94	imbi12d 346	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵)))
96		eqid 2794	. . . . . . . . . . . 12 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
97		eqid 2794	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
98	75, 14, 81, 77, 96, 63, 97	dssmapfv3d 39863	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
99		eqid 2794	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
100	75, 14, 81, 77, 96, 65, 99	dssmapfv3d 39863	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
101	98, 100	uneq12d 4063	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))
102	75, 14, 15	ntrclsfv1 39903	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
103	102	3ad2ant1 1126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐷‘𝐼) = 𝐾)
104		fveq1 6540	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
105		fveq1 6540	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
106	104, 105	uneq12d 4063	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
107	103, 106	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
108	101, 107	eqtr3d 2832	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
109	108	eqeq1d 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵 ↔ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵))
110	109	imbi2d 342	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑠 ∪ 𝑡) = 𝐵 → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
111	95, 110	bitrd 280	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
112	60, 61, 62, 111	syl3anc 1364	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
113	51, 59, 112	3bitrd 306	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
114	31, 43, 113	ralxfrd2 5207	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
115	17, 28, 114	ralxfrd2 5207	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
116	13, 115	syl5bb 284	1 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1080 = wceq 1522 ∈ wcel 2080 ∀wral 3104 ∃wrex 3105 Vcvv 3436 ∖ cdif 3858 ∪ cun 3859 ∩ cin 3860 ⊆ wss 3861 ∅c0 4213 𝒫 cpw 4455 class class class wbr 4964 ↦ cmpt 5043 ⟶wf 6224 ‘cfv 6228 (class class class)co 7019 ↑_𝑚 cmap 8259

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-rep 5084 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-ral 3109 df-rex 3110 df-reu 3111 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-pw 4457 df-sn 4475 df-pr 4477 df-op 4481 df-uni 4748 df-iun 4829 df-br 4965 df-opab 5027 df-mpt 5044 df-id 5351 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 df-fv 6236 df-ov 7022 df-oprab 7023 df-mpo 7024 df-1st 7548 df-2nd 7549 df-map 8261

This theorem is referenced by: (None)

W3C validator