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 42591

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 4201	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
2	1	eqeq1d 2733	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝑠 ∩ 𝑡) = ∅ ↔ (𝑎 ∩ 𝑡) = ∅))
3		fveq2 6878	. . . . . 6 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
4	3	ineq1d 4207	. . . . 5 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
5	4	eqeq1d 2733	. . . 4 ⊢ (𝑠 = 𝑎 → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅))
6	2, 5	imbi12d 344	. . 3 ⊢ (𝑠 = 𝑎 → (((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝑎 ∩ 𝑡) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅)))
7		ineq2 4202	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
8	7	eqeq1d 2733	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝑎 ∩ 𝑡) = ∅ ↔ (𝑎 ∩ 𝑏) = ∅))
9		fveq2 6878	. . . . . 6 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
10	9	ineq2d 4208	. . . . 5 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
11	10	eqeq1d 2733	. . . 4 ⊢ (𝑡 = 𝑏 → (((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅))
12	8, 11	imbi12d 344	. . 3 ⊢ (𝑡 = 𝑏 → (((𝑎 ∩ 𝑡) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅)))
13	6, 12	cbvral2vw 3237	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅))
14		ntrcls.d	. . . . 5 ⊢ 𝐷 = (𝑂‘𝐵)
15		ntrcls.r	. . . . 5 ⊢ (𝜑 → 𝐼𝐷𝐾)
16	14, 15	ntrclsrcomplex 42557	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18	14, 15	ntrclsrcomplex 42557	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
19	18	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
20		difeq2 4112	. . . . . 6 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
21	20	eqeq2d 2742	. . . . 5 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
22	21	adantl 482	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
23		elpwi 4603	. . . . . . 7 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
24		dfss4 4254	. . . . . . 7 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
25	23, 24	sylib 217	. . . . . 6 ⊢ (𝑎 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
26	25	eqcomd 2737	. . . . 5 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))
27	26	adantl 482	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))
28	19, 22, 27	rspcedvd 3611	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
29		simpl1 1191	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝜑)
30	14, 15	ntrclsrcomplex 42557	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
31	29, 30	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
32	14, 15	ntrclsrcomplex 42557	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
33	32	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
34		difeq2 4112	. . . . . . . 8 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
35	34	eqeq2d 2742	. . . . . . 7 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
36	35	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
37		elpwi 4603	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
38		dfss4 4254	. . . . . . . . 9 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
39	37, 38	sylib 217	. . . . . . . 8 ⊢ (𝑏 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
40	39	eqcomd 2737	. . . . . . 7 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))
41	40	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))
42	33, 36, 41	rspcedvd 3611	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
43	42	3ad2antl1 1185	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
44		simp13 1205	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑎 = (𝐵 ∖ 𝑠))
45		ineq1 4201	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
46	45	eqeq1d 2733	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝑎 ∩ 𝑏) = ∅ ↔ ((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅))
47		fveq2 6878	. . . . . . . . 9 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
48	47	ineq1d 4207	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
49	48	eqeq1d 2733	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅ ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅))
50	46, 49	imbi12d 344	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅)))
51	44, 50	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅)))
52		simp3 1138	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑏 = (𝐵 ∖ 𝑡))
53		ineq2 4202	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
54	53	eqeq1d 2733	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ ↔ ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅))
55		fveq2 6878	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
56	55	ineq2d 4208	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
57	56	eqeq1d 2733	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅ ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅))
58	54, 57	imbi12d 344	. . . . . 6 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅)))
59	52, 58	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅)))
60		simp11 1203	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
61		simp12 1204	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
62		simp2 1137	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
63		simp2 1137	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
64	63	elpwid 4605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ⊆ 𝐵)
65		simp3 1138	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
66	65	elpwid 4605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ⊆ 𝐵)
67	64, 66	unssd 4182	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
68		ssid 4000	. . . . . . . . . 10 ⊢ 𝐵 ⊆ 𝐵
69		rcompleq 4291	. . . . . . . . . 10 ⊢ (((𝑠 ∪ 𝑡) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵) → ((𝑠 ∪ 𝑡) = 𝐵 ↔ (𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵)))
70	67, 68, 69	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∪ 𝑡) = 𝐵 ↔ (𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵)))
71		difundi 4275	. . . . . . . . . 10 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
72		difid 4366	. . . . . . . . . 10 ⊢ (𝐵 ∖ 𝐵) = ∅
73	71, 72	eqeq12i 2749	. . . . . . . . 9 ⊢ ((𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵) ↔ ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅)
74	70, 73	bitr2di 287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ ↔ (𝑠 ∪ 𝑡) = 𝐵))
75		ntrcls.o	. . . . . . . . . . . . . . . 16 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
76	75, 14, 15	ntrclsiex 42575	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
77	76	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
78		elmapi 8826	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
79	77, 78	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
80	14, 15	ntrclsbex 42556	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ V)
81	80	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
82		difssd 4128	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
83	81, 82	sselpwd 5319	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
84	79, 83	ffvelcdmd 7072	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
85	84	elpwid 4605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
86		ssinss1 4233	. . . . . . . . . . 11 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
87	85, 86	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
88		0ss 4392	. . . . . . . . . 10 ⊢ ∅ ⊆ 𝐵
89		rcompleq 4291	. . . . . . . . . 10 ⊢ ((((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ ∅ ⊆ 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅)))
90	87, 88, 89	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅)))
91		difindi 4277	. . . . . . . . . 10 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
92		dif0 4368	. . . . . . . . . 10 ⊢ (𝐵 ∖ ∅) = 𝐵
93	91, 92	eqeq12i 2749	. . . . . . . . 9 ⊢ ((𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅) ↔ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵)
94	90, 93	bitrdi 286	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵))
95	74, 94	imbi12d 344	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵)))
96		eqid 2731	. . . . . . . . . . . 12 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
97		eqid 2731	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
98	75, 14, 81, 77, 96, 63, 97	dssmapfv3d 42541	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
99		eqid 2731	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
100	75, 14, 81, 77, 96, 65, 99	dssmapfv3d 42541	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
101	98, 100	uneq12d 4160	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))
102	75, 14, 15	ntrclsfv1 42577	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
103	102	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐷‘𝐼) = 𝐾)
104		fveq1 6877	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
105		fveq1 6877	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
106	104, 105	uneq12d 4160	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
107	103, 106	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
108	101, 107	eqtr3d 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
109	108	eqeq1d 2733	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵 ↔ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵))
110	109	imbi2d 340	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑠 ∪ 𝑡) = 𝐵 → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
111	95, 110	bitrd 278	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
112	60, 61, 62, 111	syl3anc 1371	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
113	51, 59, 112	3bitrd 304	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
114	31, 43, 113	ralxfrd2 5403	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
115	17, 28, 114	ralxfrd2 5403	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
116	13, 115	bitrid 282	1 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3060 ∃wrex 3069 Vcvv 3473 ∖ cdif 3941 ∪ cun 3942 ∩ cin 3943 ⊆ wss 3944 ∅c0 4318 𝒫 cpw 4596 class class class wbr 5141 ↦ cmpt 5224 ⟶wf 6528 ‘cfv 6532 (class class class)co 7393 ↑_m cmap 8803

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 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 2702 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7708

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-id 5567 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-iota 6484 df-fun 6534 df-fn 6535 df-f 6536 df-f1 6537 df-fo 6538 df-f1o 6539 df-fv 6540 df-ov 7396 df-oprab 7397 df-mpo 7398 df-1st 7957 df-2nd 7958 df-map 8805

This theorem is referenced by: (None)

W3C validator