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 44429

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 4167	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
2	1	eqeq1d 2739	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝑠 ∩ 𝑡) = ∅ ↔ (𝑎 ∩ 𝑡) = ∅))
3		fveq2 6842	. . . . . 6 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
4	3	ineq1d 4173	. . . . 5 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
5	4	eqeq1d 2739	. . . 4 ⊢ (𝑠 = 𝑎 → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅))
6	2, 5	imbi12d 344	. . 3 ⊢ (𝑠 = 𝑎 → (((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝑎 ∩ 𝑡) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅)))
7		ineq2 4168	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
8	7	eqeq1d 2739	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝑎 ∩ 𝑡) = ∅ ↔ (𝑎 ∩ 𝑏) = ∅))
9		fveq2 6842	. . . . . 6 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
10	9	ineq2d 4174	. . . . 5 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
11	10	eqeq1d 2739	. . . 4 ⊢ (𝑡 = 𝑏 → (((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅))
12	8, 11	imbi12d 344	. . 3 ⊢ (𝑡 = 𝑏 → (((𝑎 ∩ 𝑡) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅)))
13	6, 12	cbvral2vw 3220	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅))
14		ntrcls.d	. . . . 5 ⊢ 𝐷 = (𝑂‘𝐵)
15		ntrcls.r	. . . . 5 ⊢ (𝜑 → 𝐼𝐷𝐾)
16	14, 15	ntrclsrcomplex 44395	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18	14, 15	ntrclsrcomplex 44395	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
19	18	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
20		difeq2 4074	. . . . . 6 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
21	20	eqeq2d 2748	. . . . 5 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
22	21	adantl 481	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
23		elpwi 4563	. . . . . . 7 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
24		dfss4 4223	. . . . . . 7 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
25	23, 24	sylib 218	. . . . . 6 ⊢ (𝑎 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
26	25	eqcomd 2743	. . . . 5 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))
27	26	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))
28	19, 22, 27	rspcedvd 3580	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
29		simpl1 1193	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝜑)
30	14, 15	ntrclsrcomplex 44395	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
31	29, 30	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
32	14, 15	ntrclsrcomplex 44395	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
33	32	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
34		difeq2 4074	. . . . . . . 8 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
35	34	eqeq2d 2748	. . . . . . 7 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
36	35	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
37		elpwi 4563	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
38		dfss4 4223	. . . . . . . . 9 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
39	37, 38	sylib 218	. . . . . . . 8 ⊢ (𝑏 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
40	39	eqcomd 2743	. . . . . . 7 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))
41	40	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))
42	33, 36, 41	rspcedvd 3580	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
43	42	3ad2antl1 1187	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
44		simp13 1207	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑎 = (𝐵 ∖ 𝑠))
45		ineq1 4167	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
46	45	eqeq1d 2739	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝑎 ∩ 𝑏) = ∅ ↔ ((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅))
47		fveq2 6842	. . . . . . . . 9 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
48	47	ineq1d 4173	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
49	48	eqeq1d 2739	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅ ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅))
50	46, 49	imbi12d 344	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅)))
51	44, 50	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅)))
52		simp3 1139	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑏 = (𝐵 ∖ 𝑡))
53		ineq2 4168	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
54	53	eqeq1d 2739	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ ↔ ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅))
55		fveq2 6842	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
56	55	ineq2d 4174	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
57	56	eqeq1d 2739	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅ ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅))
58	54, 57	imbi12d 344	. . . . . 6 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅)))
59	52, 58	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((((𝐵 ∖ 𝑠) ∩ 𝑏) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ∅) ↔ (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅)))
60		simp11 1205	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
61		simp12 1206	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
62		simp2 1138	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
63		simp2 1138	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
64	63	elpwid 4565	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ⊆ 𝐵)
65		simp3 1139	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
66	65	elpwid 4565	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ⊆ 𝐵)
67	64, 66	unssd 4146	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
68		ssid 3958	. . . . . . . . . 10 ⊢ 𝐵 ⊆ 𝐵
69		rcompleq 4259	. . . . . . . . . 10 ⊢ (((𝑠 ∪ 𝑡) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵) → ((𝑠 ∪ 𝑡) = 𝐵 ↔ (𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵)))
70	67, 68, 69	sylancl 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∪ 𝑡) = 𝐵 ↔ (𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵)))
71		difundi 4244	. . . . . . . . . 10 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
72		difid 4330	. . . . . . . . . 10 ⊢ (𝐵 ∖ 𝐵) = ∅
73	71, 72	eqeq12i 2755	. . . . . . . . 9 ⊢ ((𝐵 ∖ (𝑠 ∪ 𝑡)) = (𝐵 ∖ 𝐵) ↔ ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅)
74	70, 73	bitr2di 288	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ ↔ (𝑠 ∪ 𝑡) = 𝐵))
75		ntrcls.o	. . . . . . . . . . . . . . . 16 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
76	75, 14, 15	ntrclsiex 44413	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
77	76	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
78		elmapi 8798	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
79	77, 78	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
80	14, 15	ntrclsbex 44394	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ V)
81	80	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
82		difssd 4091	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
83	81, 82	sselpwd 5275	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
84	79, 83	ffvelcdmd 7039	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
85	84	elpwid 4565	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
86		ssinss1 4200	. . . . . . . . . . 11 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
87	85, 86	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
88		0ss 4354	. . . . . . . . . 10 ⊢ ∅ ⊆ 𝐵
89		rcompleq 4259	. . . . . . . . . 10 ⊢ ((((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ ∅ ⊆ 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅)))
90	87, 88, 89	sylancl 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅)))
91		difindi 4246	. . . . . . . . . 10 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
92		dif0 4332	. . . . . . . . . 10 ⊢ (𝐵 ∖ ∅) = 𝐵
93	91, 92	eqeq12i 2755	. . . . . . . . 9 ⊢ ((𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = (𝐵 ∖ ∅) ↔ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵)
94	90, 93	bitrdi 287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅ ↔ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵))
95	74, 94	imbi12d 344	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵)))
96		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
97		eqid 2737	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
98	75, 14, 81, 77, 96, 63, 97	dssmapfv3d 44379	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
99		eqid 2737	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
100	75, 14, 81, 77, 96, 65, 99	dssmapfv3d 44379	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
101	98, 100	uneq12d 4123	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))
102	75, 14, 15	ntrclsfv1 44415	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
103	102	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐷‘𝐼) = 𝐾)
104		fveq1 6841	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
105		fveq1 6841	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
106	104, 105	uneq12d 4123	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
107	103, 106	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
108	101, 107	eqtr3d 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
109	108	eqeq1d 2739	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵 ↔ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵))
110	109	imbi2d 340	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑠 ∪ 𝑡) = 𝐵 → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = 𝐵) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
111	95, 110	bitrd 279	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
112	60, 61, 62, 111	syl3anc 1374	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) = ∅ → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
113	51, 59, 112	3bitrd 305	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
114	31, 43, 113	ralxfrd2 5359	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
115	17, 28, 114	ralxfrd2 5359	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝑎 ∩ 𝑏) = ∅ → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
116	13, 115	bitrid 283	1 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 Vcvv 3442 ∖ cdif 3900 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 ∅c0 4287 𝒫 cpw 4556 class class class wbr 5100 ↦ cmpt 5181 ⟶wf 6496 ‘cfv 6500 (class class class)co 7368 ↑_m cmap 8775

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-ov 7371 df-oprab 7372 df-mpo 7373 df-1st 7943 df-2nd 7944 df-map 8777

This theorem is referenced by: (None)

W3C validator