ntrclsk13 - Mathbox for Richard Penner

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

Theorem ntrclsk13 42333

Description: The interior of the intersection of any pair is equal to the intersection of the interiors if and only if the closure of the unions of any pair is equal to the union of closures. (Contributed by RP, 19-Jun-2021.)

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

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

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

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

Step	Hyp	Ref	Expression
1		ineq1 4165	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
2	1	fveq2d 6846	. . . 4 ⊢ (𝑠 = 𝑎 → (𝐼‘(𝑠 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑡)))
3		fveq2 6842	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
4	3	ineq1d 4171	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
5	2, 4	eqeq12d 2752	. . 3 ⊢ (𝑠 = 𝑎 → ((𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ (𝐼‘(𝑎 ∩ 𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡))))
6		ineq2 4166	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
7	6	fveq2d 6846	. . . 4 ⊢ (𝑡 = 𝑏 → (𝐼‘(𝑎 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑏)))
8		fveq2 6842	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
9	8	ineq2d 4172	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
10	7, 9	eqeq12d 2752	. . 3 ⊢ (𝑡 = 𝑏 → ((𝐼‘(𝑎 ∩ 𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ↔ (𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏))))
11	5, 10	cbvral2vw 3227	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
12		ntrcls.d	. . . . . 6 ⊢ 𝐷 = (𝑂‘𝐵)
13		ntrcls.r	. . . . . 6 ⊢ (𝜑 → 𝐼𝐷𝐾)
14	12, 13	ntrclsbex 42296	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
15		difssd 4092	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ⊆ 𝐵)
16	14, 15	sselpwd 5283	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18		elpwi 4567	. . . 4 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
19	14	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → 𝐵 ∈ V)
20		difssd 4092	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ⊆ 𝐵)
21	19, 20	sselpwd 5283	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
22		difeq2 4076	. . . . . . . 8 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
23	22	eqeq2d 2747	. . . . . . 7 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
24		eqcom 2743	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
25	23, 24	bitrdi 286	. . . . . 6 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎))
26	25	adantl 482	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎))
27		dfss4 4218	. . . . . . 7 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
28	27	biimpi 215	. . . . . 6 ⊢ (𝑎 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
29	28	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
30	21, 26, 29	rspcedvd 3583	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
31	18, 30	sylan2 593	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
32		ineq1 4165	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
33	32	fveq2d 6846	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘(𝑎 ∩ 𝑏)) = (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)))
34		fveq2 6842	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
35	34	ineq1d 4171	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
36	33, 35	eqeq12d 2752	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
37	36	ralbidv 3174	. . . . 5 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
38	37	3ad2ant3 1135	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
39		difssd 4092	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ⊆ 𝐵)
40	14, 39	sselpwd 5283	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
41	40	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
42		simpll 765	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝜑)
43		elpwi 4567	. . . . . . . 8 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
44	43	adantl 482	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏 ⊆ 𝐵)
45		difssd 4092	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ⊆ 𝐵)
46	14, 45	sselpwd 5283	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
47	46	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
48		difeq2 4076	. . . . . . . . . . 11 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
49	48	eqeq2d 2747	. . . . . . . . . 10 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
50		eqcom 2743	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
51	49, 50	bitrdi 286	. . . . . . . . 9 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏))
52	51	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏))
53		dfss4 4218	. . . . . . . . . 10 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
54	53	biimpi 215	. . . . . . . . 9 ⊢ (𝑏 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
55	54	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
56	47, 52, 55	rspcedvd 3583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
57	42, 44, 56	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
58		ineq2 4166	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
59		difundi 4239	. . . . . . . . . . 11 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
60	58, 59	eqtr4di 2794	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠 ∪ 𝑡)))
61	60	fveq2d 6846	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))
62		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
63	62	ineq2d 4172	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
64	61, 63	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
65	64	3ad2ant3 1135	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
66		simp1l 1197	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
67	66, 14	jccir 522	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (𝜑 ∧ 𝐵 ∈ V))
68		simp1r 1198	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
69		simp2 1137	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
70		ntrcls.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
71	70, 12, 13	ntrclsiex 42315	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
72		elmapi 8787	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
73	71, 72	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
74	73	anim1i 615	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ∈ V) → (𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V))
75	74	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V))
76		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
77		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → 𝐵 ∈ V)
78		difssd 4092	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ⊆ 𝐵)
79	77, 78	sselpwd 5283	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ∈ 𝒫 𝐵)
80	76, 79	ffvelcdmd 7036	. . . . . . . . . . . 12 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ∈ 𝒫 𝐵)
81	80	elpwid 4569	. . . . . . . . . . 11 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵)
82		difssd 4092	. . . . . . . . . . . . . . 15 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
83	77, 82	sselpwd 5283	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
84	76, 83	ffvelcdmd 7036	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
85	84	elpwid 4569	. . . . . . . . . . . 12 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
86		ssinss1 4197	. . . . . . . . . . . 12 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
87	85, 86	syl 17	. . . . . . . . . . 11 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
88	81, 87	jca 512	. . . . . . . . . 10 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵))
89		rcompleq 4255	. . . . . . . . . 10 ⊢ (((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
90	75, 88, 89	3syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
91		simplr 767	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
92	71	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
93		eqid 2736	. . . . . . . . . . 11 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
94		simprl 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
95	94	elpwid 4569	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ⊆ 𝐵)
96		simprr 771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
97	96	elpwid 4569	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ⊆ 𝐵)
98	95, 97	unssd 4146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
99	91, 98	sselpwd 5283	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵)
100		eqid 2736	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡))
101	70, 12, 91, 92, 93, 99, 100	dssmapfv3d 42281	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
102		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
103		simplr 767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
104	71	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
105		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
106		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
107	70, 12, 103, 104, 93, 105, 106	dssmapfv3d 42281	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
108	102, 107	sylan2 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
109		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
110		simplr 767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
111	71	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
112		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
113		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
114	70, 12, 110, 111, 93, 112, 113	dssmapfv3d 42281	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
115	109, 114	sylan2 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
116	108, 115	uneq12d 4124	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))
117		difindi 4241	. . . . . . . . . . 11 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
118	116, 117	eqtr4di 2794	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
119	101, 118	eqeq12d 2752	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
120		simpll 765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝜑)
121	70, 12, 13	ntrclsfv1 42317	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
122		fveq1 6841	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡)))
123		fveq1 6841	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
124		fveq1 6841	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
125	123, 124	uneq12d 4124	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
126	122, 125	eqeq12d 2752	. . . . . . . . . 10 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
127	120, 121, 126	3syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
128	90, 119, 127	3bitr2d 306	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
129	67, 68, 69, 128	syl12anc 835	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
130	65, 129	bitrd 278	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
131	41, 57, 130	ralxfrd2 5367	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
132	131	3adant3 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
133	38, 132	bitrd 278	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
134	17, 31, 133	ralxfrd2 5367	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
135	11, 134	bitrid 282	1 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3064 ∃wrex 3073 Vcvv 3445 ∖ cdif 3907 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 𝒫 cpw 4560 class class class wbr 5105 ↦ cmpt 5188 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 ↑_m cmap 8765

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 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672

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 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-ov 7360 df-oprab 7361 df-mpo 7362 df-1st 7921 df-2nd 7922 df-map 8767

This theorem is referenced by: (None)

W3C validator