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 41679

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 ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
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 4139	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
2	1	eqeq1d 2740	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝑠 ∩ 𝑡) = ∅ ↔ (𝑎 ∩ 𝑡) = ∅))
3		fveq2 6774	. . . . . 6 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
4	3	ineq1d 4145	. . . . 5 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
5	4	eqeq1d 2740	. . . 4 ⊢ (𝑠 = 𝑎 → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅))
6	2, 5	imbi12d 345	. . 3 ⊢ (𝑠 = 𝑎 → (((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝑎 ∩ 𝑡) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅)))
7		ineq2 4140	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
8	7	eqeq1d 2740	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝑎 ∩ 𝑡) = ∅ ↔ (𝑎 ∩ 𝑏) = ∅))
9		fveq2 6774	. . . . . 6 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
10	9	ineq2d 4146	. . . . 5 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
11	10	eqeq1d 2740	. . . 4 ⊢ (𝑡 = 𝑏 → (((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅))
12	8, 11	imbi12d 345	. . 3 ⊢ (𝑡 = 𝑏 → (((𝑎 ∩ 𝑡) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅)))
13	6, 12	cbvral2vw 3396	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅))
14		ntrcls.d	. . . . 5 ⊢ 𝐷 = (𝑂‘𝐵)
15		ntrcls.r	. . . . 5 ⊢ (𝜑 → 𝐼𝐷𝐾)
16	14, 15	ntrclsrcomplex 41645	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18	14, 15	ntrclsrcomplex 41645	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
19	18	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
20		difeq2 4051	. . . . . 6 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
21	20	eqeq2d 2749	. . . . 5 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
22	21	adantl 482	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
23		elpwi 4542	. . . . . . 7 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
24		dfss4 4192	. . . . . . 7 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
25	23, 24	sylib 217	. . . . . 6 ⊢ (𝑎 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
26	25	eqcomd 2744	. . . . 5 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))
27	26	adantl 482	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))
28	19, 22, 27	rspcedvd 3563	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
29		simpl1 1190	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝜑)
30	14, 15	ntrclsrcomplex 41645	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
31	29, 30	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
32	14, 15	ntrclsrcomplex 41645	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
33	32	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
34		difeq2 4051	. . . . . . . 8 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
35	34	eqeq2d 2749	. . . . . . 7 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
36	35	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
37		elpwi 4542	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
38		dfss4 4192	. . . . . . . . 9 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
39	37, 38	sylib 217	. . . . . . . 8 ⊢ (𝑏 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
40	39	eqcomd 2744	. . . . . . 7 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))
41	40	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))
42	33, 36, 41	rspcedvd 3563	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
43	42	3ad2antl1 1184	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
44		simp13 1204	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑎 = (𝐵 ∖ 𝑠))
45		ineq1 4139	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
46	45	eqeq1d 2740	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝑎 ∩ 𝑏) = ∅ ↔ ((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅))
47		fveq2 6774	. . . . . . . . 9 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
48	47	ineq1d 4145	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
49	48	eqeq1d 2740	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅ ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅))
50	46, 49	imbi12d 345	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅)))
51	44, 50	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅)))
52		simp3 1137	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑏 = (𝐵 ∖ 𝑡))
53		ineq2 4140	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
54	53	eqeq1d 2740	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ ↔ ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅))
55		fveq2 6774	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
56	55	ineq2d 4146	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
57	56	eqeq1d 2740	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅ ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅))
58	54, 57	imbi12d 345	. . . . . 6 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅)))
59	52, 58	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅)))
60		simp11 1202	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
61		simp12 1203	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
62		simp2 1136	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
63		simp2 1136	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
64	63	elpwid 4544	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ⊆ 𝐵)
65		simp3 1137	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
66	65	elpwid 4544	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ⊆ 𝐵)
67	64, 66	unssd 4120	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
68		ssid 3943	. . . . . . . . . 10 ⊢ 𝐵 ⊆ 𝐵
69		rcompleq 4229	. . . . . . . . . 10 ⊢ (((𝑠 ∪ 𝑡) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵) → ((𝑠 ∪ 𝑡) = 𝐵 ↔ (𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵)))
70	67, 68, 69	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∪ 𝑡) = 𝐵 ↔ (𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵)))
71		difundi 4213	. . . . . . . . . 10 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
72		difid 4304	. . . . . . . . . 10 ⊢ (𝐵 ∖ 𝐵) = ∅
73	71, 72	eqeq12i 2756	. . . . . . . . 9 ⊢ ((𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵) ↔ ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅)
74	70, 73	bitr2di 288	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ ↔ (𝑠 ∪ 𝑡) = 𝐵))
75		ntrcls.o	. . . . . . . . . . . . . . . 16 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
76	75, 14, 15	ntrclsiex 41663	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
77	76	3ad2ant1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
78		elmapi 8637	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
79	77, 78	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
80	14, 15	ntrclsbex 41644	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ V)
81	80	3ad2ant1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
82		difssd 4067	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
83	81, 82	sselpwd 5250	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
84	79, 83	ffvelrnd 6962	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
85	84	elpwid 4544	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
86		ssinss1 4171	. . . . . . . . . . 11 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
87	85, 86	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
88		0ss 4330	. . . . . . . . . 10 ⊢ ∅ ⊆ 𝐵
89		rcompleq 4229	. . . . . . . . . 10 ⊢ ((((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ ∅ ⊆ 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅)))
90	87, 88, 89	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅)))
91		difindi 4215	. . . . . . . . . 10 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
92		dif0 4306	. . . . . . . . . 10 ⊢ (𝐵 ∖ ∅) = 𝐵
93	91, 92	eqeq12i 2756	. . . . . . . . 9 ⊢ ((𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅) ↔ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵)
94	90, 93	bitrdi 287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵))
95	74, 94	imbi12d 345	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵)))
96		eqid 2738	. . . . . . . . . . . 12 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
97		eqid 2738	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
98	75, 14, 81, 77, 96, 63, 97	dssmapfv3d 41627	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
99		eqid 2738	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
100	75, 14, 81, 77, 96, 65, 99	dssmapfv3d 41627	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
101	98, 100	uneq12d 4098	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))
102	75, 14, 15	ntrclsfv1 41665	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
103	102	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐷‘𝐼) = 𝐾)
104		fveq1 6773	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
105		fveq1 6773	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
106	104, 105	uneq12d 4098	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
107	103, 106	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
108	101, 107	eqtr3d 2780	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
109	108	eqeq1d 2740	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵 ↔ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵))
110	109	imbi2d 341	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑠 ∪ 𝑡) = 𝐵 → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
111	95, 110	bitrd 278	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
112	60, 61, 62, 111	syl3anc 1370	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
113	51, 59, 112	3bitrd 305	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
114	31, 43, 113	ralxfrd2 5335	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
115	17, 28, 114	ralxfrd2 5335	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
116	13, 115	bitrid 282	1 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 Vcvv 3432 ∖ cdif 3884 ∪ cun 3885 ∩ cin 3886 ⊆ wss 3887 ∅c0 4256 𝒫 cpw 4533 class class class wbr 5074 ↦ cmpt 5157 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 ↑_m cmap 8615

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-ov 7278 df-oprab 7279 df-mpo 7280 df-1st 7831 df-2nd 7832 df-map 8617

This theorem is referenced by: (None)

W3C validator