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 44067

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 4179	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
2	1	fveq2d 6865	. . . 4 ⊢ (𝑠 = 𝑎 → (𝐼‘(𝑠 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑡)))
3		fveq2 6861	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
4	3	ineq1d 4185	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
5	2, 4	eqeq12d 2746	. . 3 ⊢ (𝑠 = 𝑎 → ((𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ (𝐼‘(𝑎 ∩ 𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡))))
6		ineq2 4180	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
7	6	fveq2d 6865	. . . 4 ⊢ (𝑡 = 𝑏 → (𝐼‘(𝑎 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑏)))
8		fveq2 6861	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
9	8	ineq2d 4186	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
10	7, 9	eqeq12d 2746	. . 3 ⊢ (𝑡 = 𝑏 → ((𝐼‘(𝑎 ∩ 𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ↔ (𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏))))
11	5, 10	cbvral2vw 3220	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
12		ntrcls.d	. . . . . 6 ⊢ 𝐷 = (𝑂‘𝐵)
13		ntrcls.r	. . . . . 6 ⊢ (𝜑 → 𝐼𝐷𝐾)
14	12, 13	ntrclsbex 44030	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
15		difssd 4103	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ⊆ 𝐵)
16	14, 15	sselpwd 5286	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18		elpwi 4573	. . . 4 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
19	14	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → 𝐵 ∈ V)
20		difssd 4103	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ⊆ 𝐵)
21	19, 20	sselpwd 5286	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
22		difeq2 4086	. . . . . . . 8 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
23	22	eqeq2d 2741	. . . . . . 7 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
24		eqcom 2737	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
25	23, 24	bitrdi 287	. . . . . 6 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎))
26	25	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎))
27		dfss4 4235	. . . . . . 7 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
28	27	biimpi 216	. . . . . 6 ⊢ (𝑎 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
29	28	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
30	21, 26, 29	rspcedvd 3593	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
31	18, 30	sylan2 593	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
32		ineq1 4179	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
33	32	fveq2d 6865	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘(𝑎 ∩ 𝑏)) = (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)))
34		fveq2 6861	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
35	34	ineq1d 4185	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
36	33, 35	eqeq12d 2746	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
37	36	ralbidv 3157	. . . . 5 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
38	37	3ad2ant3 1135	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
39		difssd 4103	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ⊆ 𝐵)
40	14, 39	sselpwd 5286	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
41	40	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
42		simpll 766	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝜑)
43		elpwi 4573	. . . . . . . 8 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
44	43	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏 ⊆ 𝐵)
45		difssd 4103	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ⊆ 𝐵)
46	14, 45	sselpwd 5286	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
47	46	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
48		difeq2 4086	. . . . . . . . . . 11 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
49	48	eqeq2d 2741	. . . . . . . . . 10 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
50		eqcom 2737	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
51	49, 50	bitrdi 287	. . . . . . . . 9 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏))
52	51	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏))
53		dfss4 4235	. . . . . . . . . 10 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
54	53	biimpi 216	. . . . . . . . 9 ⊢ (𝑏 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
55	54	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
56	47, 52, 55	rspcedvd 3593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
57	42, 44, 56	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
58		ineq2 4180	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
59		difundi 4256	. . . . . . . . . . 11 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
60	58, 59	eqtr4di 2783	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠 ∪ 𝑡)))
61	60	fveq2d 6865	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))
62		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
63	62	ineq2d 4186	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
64	61, 63	eqeq12d 2746	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
65	64	3ad2ant3 1135	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
66		simp1l 1198	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
67	66, 14	jccir 521	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (𝜑 ∧ 𝐵 ∈ V))
68		simp1r 1199	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
69		simp2 1137	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
70		ntrcls.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
71	70, 12, 13	ntrclsiex 44049	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
72		elmapi 8825	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
73	71, 72	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
74	73	anim1i 615	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ∈ V) → (𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V))
75	74	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V))
76		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
77		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → 𝐵 ∈ V)
78		difssd 4103	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ⊆ 𝐵)
79	77, 78	sselpwd 5286	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ∈ 𝒫 𝐵)
80	76, 79	ffvelcdmd 7060	. . . . . . . . . . . 12 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ∈ 𝒫 𝐵)
81	80	elpwid 4575	. . . . . . . . . . 11 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵)
82		difssd 4103	. . . . . . . . . . . . . . 15 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
83	77, 82	sselpwd 5286	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
84	76, 83	ffvelcdmd 7060	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
85	84	elpwid 4575	. . . . . . . . . . . 12 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
86		ssinss1 4212	. . . . . . . . . . . 12 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
87	85, 86	syl 17	. . . . . . . . . . 11 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
88	81, 87	jca 511	. . . . . . . . . 10 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵))
89		rcompleq 4271	. . . . . . . . . 10 ⊢ (((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
90	75, 88, 89	3syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
91		simplr 768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
92	71	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
93		eqid 2730	. . . . . . . . . . 11 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
94		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
95	94	elpwid 4575	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ⊆ 𝐵)
96		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
97	96	elpwid 4575	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ⊆ 𝐵)
98	95, 97	unssd 4158	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
99	91, 98	sselpwd 5286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵)
100		eqid 2730	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡))
101	70, 12, 91, 92, 93, 99, 100	dssmapfv3d 44015	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
102		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
103		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
104	71	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
105		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
106		eqid 2730	. . . . . . . . . . . . . 14 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
107	70, 12, 103, 104, 93, 105, 106	dssmapfv3d 44015	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
108	102, 107	sylan2 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
109		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
110		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
111	71	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
112		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
113		eqid 2730	. . . . . . . . . . . . . 14 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
114	70, 12, 110, 111, 93, 112, 113	dssmapfv3d 44015	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
115	109, 114	sylan2 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
116	108, 115	uneq12d 4135	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))
117		difindi 4258	. . . . . . . . . . 11 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
118	116, 117	eqtr4di 2783	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
119	101, 118	eqeq12d 2746	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
120		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝜑)
121	70, 12, 13	ntrclsfv1 44051	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
122		fveq1 6860	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡)))
123		fveq1 6860	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
124		fveq1 6860	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
125	123, 124	uneq12d 4135	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
126	122, 125	eqeq12d 2746	. . . . . . . . . 10 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
127	120, 121, 126	3syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
128	90, 119, 127	3bitr2d 307	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
129	67, 68, 69, 128	syl12anc 836	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
130	65, 129	bitrd 279	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
131	41, 57, 130	ralxfrd2 5370	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
132	131	3adant3 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
133	38, 132	bitrd 279	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
134	17, 31, 133	ralxfrd2 5370	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
135	11, 134	bitrid 283	1 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3045 ∃wrex 3054 Vcvv 3450 ∖ cdif 3914 ∪ cun 3915 ∩ cin 3916 ⊆ wss 3917 𝒫 cpw 4566 class class class wbr 5110 ↦ cmpt 5191 ⟶wf 6510 ‘cfv 6514 (class class class)co 7390 ↑_m cmap 8802

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-id 5536 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-ov 7393 df-oprab 7394 df-mpo 7395 df-1st 7971 df-2nd 7972 df-map 8804

This theorem is referenced by: (None)

W3C validator