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 40412

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 4180	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
2	1	eqeq1d 2823	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝑠 ∩ 𝑡) = ∅ ↔ (𝑎 ∩ 𝑡) = ∅))
3		fveq2 6664	. . . . . 6 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
4	3	ineq1d 4187	. . . . 5 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
5	4	eqeq1d 2823	. . . 4 ⊢ (𝑠 = 𝑎 → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅))
6	2, 5	imbi12d 347	. . 3 ⊢ (𝑠 = 𝑎 → (((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝑎 ∩ 𝑡) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅)))
7		ineq2 4182	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
8	7	eqeq1d 2823	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝑎 ∩ 𝑡) = ∅ ↔ (𝑎 ∩ 𝑏) = ∅))
9		fveq2 6664	. . . . . 6 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
10	9	ineq2d 4188	. . . . 5 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
11	10	eqeq1d 2823	. . . 4 ⊢ (𝑡 = 𝑏 → (((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅))
12	8, 11	imbi12d 347	. . 3 ⊢ (𝑡 = 𝑏 → (((𝑎 ∩ 𝑡) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅)))
13	6, 12	cbvral2vw 3461	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅))
14		ntrcls.d	. . . . 5 ⊢ 𝐷 = (𝑂‘𝐵)
15		ntrcls.r	. . . . 5 ⊢ (𝜑 → 𝐼𝐷𝐾)
16	14, 15	ntrclsrcomplex 40378	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 483	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18	14, 15	ntrclsrcomplex 40378	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
19	18	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
20		difeq2 4092	. . . . . 6 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
21	20	eqeq2d 2832	. . . . 5 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
22	21	adantl 484	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
23		elpwi 4550	. . . . . . 7 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
24		dfss4 4234	. . . . . . 7 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
25	23, 24	sylib 220	. . . . . 6 ⊢ (𝑎 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
26	25	eqcomd 2827	. . . . 5 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))
27	26	adantl 484	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))
28	19, 22, 27	rspcedvd 3625	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
29		simpl1 1187	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝜑)
30	14, 15	ntrclsrcomplex 40378	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
31	29, 30	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
32	14, 15	ntrclsrcomplex 40378	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
33	32	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
34		difeq2 4092	. . . . . . . 8 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
35	34	eqeq2d 2832	. . . . . . 7 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
36	35	adantl 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
37		elpwi 4550	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
38		dfss4 4234	. . . . . . . . 9 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
39	37, 38	sylib 220	. . . . . . . 8 ⊢ (𝑏 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
40	39	eqcomd 2827	. . . . . . 7 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))
41	40	adantl 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))
42	33, 36, 41	rspcedvd 3625	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
43	42	3ad2antl1 1181	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
44		simp13 1201	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑎 = (𝐵 ∖ 𝑠))
45		ineq1 4180	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
46	45	eqeq1d 2823	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝑎 ∩ 𝑏) = ∅ ↔ ((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅))
47		fveq2 6664	. . . . . . . . 9 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
48	47	ineq1d 4187	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
49	48	eqeq1d 2823	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅ ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅))
50	46, 49	imbi12d 347	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅)))
51	44, 50	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅)))
52		simp3 1134	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑏 = (𝐵 ∖ 𝑡))
53		ineq2 4182	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
54	53	eqeq1d 2823	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ ↔ ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅))
55		fveq2 6664	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
56	55	ineq2d 4188	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
57	56	eqeq1d 2823	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅ ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅))
58	54, 57	imbi12d 347	. . . . . 6 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅)))
59	52, 58	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅)))
60		simp11 1199	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
61		simp12 1200	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
62		simp2 1133	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
63		simp2 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
64	63	elpwid 4552	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ⊆ 𝐵)
65		simp3 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
66	65	elpwid 4552	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ⊆ 𝐵)
67	64, 66	unssd 4161	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
68		ssid 3988	. . . . . . . . . 10 ⊢ 𝐵 ⊆ 𝐵
69		rcompleq 40363	. . . . . . . . . 10 ⊢ (((𝑠 ∪ 𝑡) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵) → ((𝑠 ∪ 𝑡) = 𝐵 ↔ (𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵)))
70	67, 68, 69	sylancl 588	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∪ 𝑡) = 𝐵 ↔ (𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵)))
71		difundi 4255	. . . . . . . . . 10 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
72		difid 4329	. . . . . . . . . 10 ⊢ (𝐵 ∖ 𝐵) = ∅
73	71, 72	eqeq12i 2836	. . . . . . . . 9 ⊢ ((𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵) ↔ ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅)
74	70, 73	syl6rbb 290	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ ↔ (𝑠 ∪ 𝑡) = 𝐵))
75		ntrcls.o	. . . . . . . . . . . . . . . 16 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
76	75, 14, 15	ntrclsiex 40396	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
77	76	3ad2ant1 1129	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
78		elmapi 8422	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
79	77, 78	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
80	14, 15	ntrclsbex 40377	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ V)
81	80	3ad2ant1 1129	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
82		difssd 4108	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
83	81, 82	sselpwd 5222	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
84	79, 83	ffvelrnd 6846	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
85	84	elpwid 4552	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
86		ssinss1 4213	. . . . . . . . . . 11 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
87	85, 86	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
88		0ss 4349	. . . . . . . . . 10 ⊢ ∅ ⊆ 𝐵
89		rcompleq 40363	. . . . . . . . . 10 ⊢ ((((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ ∅ ⊆ 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅)))
90	87, 88, 89	sylancl 588	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅)))
91		difindi 4257	. . . . . . . . . 10 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
92		dif0 4331	. . . . . . . . . 10 ⊢ (𝐵 ∖ ∅) = 𝐵
93	91, 92	eqeq12i 2836	. . . . . . . . 9 ⊢ ((𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅) ↔ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵)
94	90, 93	syl6bb 289	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵))
95	74, 94	imbi12d 347	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵)))
96		eqid 2821	. . . . . . . . . . . 12 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
97		eqid 2821	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
98	75, 14, 81, 77, 96, 63, 97	dssmapfv3d 40358	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
99		eqid 2821	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
100	75, 14, 81, 77, 96, 65, 99	dssmapfv3d 40358	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
101	98, 100	uneq12d 4139	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))
102	75, 14, 15	ntrclsfv1 40398	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
103	102	3ad2ant1 1129	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐷‘𝐼) = 𝐾)
104		fveq1 6663	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
105		fveq1 6663	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
106	104, 105	uneq12d 4139	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
107	103, 106	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
108	101, 107	eqtr3d 2858	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
109	108	eqeq1d 2823	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵 ↔ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵))
110	109	imbi2d 343	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑠 ∪ 𝑡) = 𝐵 → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
111	95, 110	bitrd 281	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
112	60, 61, 62, 111	syl3anc 1367	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
113	51, 59, 112	3bitrd 307	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
114	31, 43, 113	ralxfrd2 5304	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
115	17, 28, 114	ralxfrd2 5304	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
116	13, 115	syl5bb 285	1 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ∀wral 3138 ∃wrex 3139 Vcvv 3494 ∖ cdif 3932 ∪ cun 3933 ∩ cin 3934 ⊆ wss 3935 ∅c0 4290 𝒫 cpw 4538 class class class wbr 5058 ↦ cmpt 5138 ⟶wf 6345 ‘cfv 6349 (class class class)co 7150 ↑_m cmap 8400

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-ov 7153 df-oprab 7154 df-mpo 7155 df-1st 7683 df-2nd 7684 df-map 8402

This theorem is referenced by: (None)

W3C validator