ntrclsk3 - Mathbox for Richard Penner

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

Theorem ntrclsk3 45262

Description: The intersection of interiors of a every pair is a subset of the interior of the intersection of the pair if an only if the closure of the union of every pair is a subset of the union of closures of the pair. (Contributed by RP, 19-Jun-2021.)

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

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

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

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

Step	Hyp	Ref	Expression
1		fveq2 6908	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
2	1	ineq1d 4119	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
3		ineq1 4113	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
4	3	fveq2d 6912	. . . 4 ⊢ (𝑠 = 𝑎 → (𝐼‘(𝑠 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑡)))
5	2, 4	sseq12d 3946	. . 3 ⊢ (𝑠 = 𝑎 → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑎 ∩ 𝑡))))
6		fveq2 6908	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
7	6	ineq2d 4120	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
8		ineq2 4114	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
9	8	fveq2d 6912	. . . 4 ⊢ (𝑡 = 𝑏 → (𝐼‘(𝑎 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑏)))
10	7, 9	sseq12d 3946	. . 3 ⊢ (𝑡 = 𝑏 → (((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑎 ∩ 𝑡)) ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏))))
11	5, 10	cbvral2vw 3248	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)))
12		ntrcls.d	. . . . . 6 ⊢ 𝐷 = (𝑂‘𝐵)
13		ntrcls.r	. . . . . 6 ⊢ (𝜑 → 𝐼𝐷𝐾)
14	12, 13	ntrclsbex 45226	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
15		difssd 4076	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ⊆ 𝐵)
16	14, 15	sselpwd 5294	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18		elpwi 4567	. . . 4 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
19		simpl 488	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → 𝐵 ∈ V)
20		difssd 4076	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ⊆ 𝐵)
21	19, 20	sselpwd 5294	. . . . 5 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
22		simpr 490	. . . . . . . 8 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → 𝑠 = (𝐵 ∖ 𝑎))
23	22	difeq2d 4066	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
24	23	eqeq2d 2774	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
25		eqcom 2770	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
26	24, 25	bitrdi 290	. . . . 5 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎))
27		dfss4 4217	. . . . . 6 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
28	27	bilani 510	. . . . 5 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
29	21, 26, 28	rspcedvd 3582	. . . 4 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
30	14, 18, 29	syl2an 608	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
31		simpl1 1210	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝜑)
32		difssd 4076	. . . . . 6 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ⊆ 𝐵)
33	14, 32	sselpwd 5294	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
34	31, 33	syl 18	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
35		elpwi 4567	. . . . . 6 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
36		simpl 488	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → 𝐵 ∈ V)
37		difssd 4076	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ⊆ 𝐵)
38	36, 37	sselpwd 5294	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
39		simpr 490	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → 𝑡 = (𝐵 ∖ 𝑏))
40	39	difeq2d 4066	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
41	40	eqeq2d 2774	. . . . . . . 8 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
42		eqcom 2770	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
43	41, 42	bitrdi 290	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏))
44		dfss4 4217	. . . . . . . 8 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
45	44	bilani 510	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
46	38, 43, 45	rspcedvd 3582	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
47	14, 35, 46	syl2an 608	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
48	47	3ad2antl1 1204	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
49		simp13 1224	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑎 = (𝐵 ∖ 𝑠))
50		fveq2 6908	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
51	50	ineq1d 4119	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
52		ineq1 4113	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
53	52	fveq2d 6912	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘(𝑎 ∩ 𝑏)) = (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)))
54	51, 53	sseq12d 3946	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏))))
55	49, 54	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏))))
56		fveq2 6908	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
57	56	ineq2d 4120	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
58		ineq2 4114	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
59		difundi 4238	. . . . . . . . 9 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
60	58, 59	eqtr4di 2816	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠 ∪ 𝑡)))
61	60	fveq2d 6912	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))
62	57, 61	sseq12d 3946	. . . . . 6 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
63	62	3ad2ant3 1153	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
64		simp11 1222	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
65		ntrcls.o	. . . . . . . . 9 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
66	65, 12, 13	ntrclsiex 45245	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
67	66, 14	jca 521	. . . . . . 7 ⊢ (𝜑 → (𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V))
68		elmapi 8897	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
69	68	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
70		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → 𝐵 ∈ V)
71		difssd 4076	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
72	70, 71	sselpwd 5294	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
73	69, 72	ffvelcdmd 7109	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
74	73	elpwid 4569	. . . . . . . . 9 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
75		orc 881	. . . . . . . . 9 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ∨ (𝐼‘(𝐵 ∖ 𝑡)) ⊆ 𝐵))
76		inss 4148	. . . . . . . . 9 ⊢ (((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ∨ (𝐼‘(𝐵 ∖ 𝑡)) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
77	74, 75, 76	3syl 19	. . . . . . . 8 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
78		difssd 4076	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ⊆ 𝐵)
79	70, 78	sselpwd 5294	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ∈ 𝒫 𝐵)
80	69, 79	ffvelcdmd 7109	. . . . . . . . 9 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ∈ 𝒫 𝐵)
81	80	elpwid 4569	. . . . . . . 8 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵)
82	77, 81	jca 521	. . . . . . 7 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵))
83		sscon34b 4252	. . . . . . 7 ⊢ ((((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
84	64, 67, 82, 83	4syl 20	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
85		difindi 4240	. . . . . . . 8 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
86	85	sseq2i 3942	. . . . . . 7 ⊢ ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))
87	86	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))))
88	64, 14	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝐵 ∈ V)
89	64, 66	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
90		simp12 1223	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
91		rp-simp2 44985	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
92		simpl2 1211	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
93		simpl3 1212	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
94		eqid 2763	. . . . . . . . . 10 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
95		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
96		simprl 783	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
97	96	elpwid 4569	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ⊆ 𝐵)
98		simprr 785	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
99	98	elpwid 4569	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ⊆ 𝐵)
100	97, 99	unssd 4193	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
101	95, 100	sselpwd 5294	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵)
102	101	3ad2antl2 1205	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵)
103		eqid 2763	. . . . . . . . . 10 ⊢ ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡))
104	65, 12, 92, 93, 94, 102, 103	dssmapfv3d 45211	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
105		simpl1 1210	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝜑)
106	65, 12, 13	ntrclsfv1 45247	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
107	106	fveq1d 6910	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡)))
108	105, 107	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡)))
109	104, 108	eqtr3d 2800	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐾‘(𝑠 ∪ 𝑡)))
110		simprl 783	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
111		eqid 2763	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
112	65, 12, 92, 93, 94, 110, 111	dssmapfv3d 45211	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
113	106	fveq1d 6910	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
114	105, 113	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
115	112, 114	eqtr3d 2800	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) = (𝐾‘𝑠))
116		simprr 785	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
117		eqid 2763	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
118	65, 12, 92, 93, 94, 116, 117	dssmapfv3d 45211	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
119	106	fveq1d 6910	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
120	105, 119	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
121	118, 120	eqtr3d 2800	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))) = (𝐾‘𝑡))
122	115, 121	uneq12d 4171	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
123	109, 122	sseq12d 3946	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
124	64, 88, 89, 90, 91, 123	syl32anc 1406	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
125	84, 87, 124	3bitrd 308	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
126	55, 63, 125	3bitrd 308	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
127	34, 48, 126	ralxfrd2 5378	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
128	17, 30, 127	ralxfrd2 5378	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
129	11, 128	bitrid 286	1 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 ∪ cun 4152 𝒫 cpw 4560 class class class wbr 5106 ↦ cmpt 5189 ⟶wf 6554 ‘cfv 6558 (class class class)co 7443 ↑_m cmap 8875

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-frege1 44982

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-ov 7446 df-oprab 7447 df-mpo 7448 df-1st 8025 df-2nd 8026 df-map 8877

This theorem is used by: (None)

W3C validator