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 44828

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 6885	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
2	1	ineq1d 4175	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
3		ineq1 4169	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
4	3	fveq2d 6889	. . . 4 ⊢ (𝑠 = 𝑎 → (𝐼‘(𝑠 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑡)))
5	2, 4	sseq12d 3973	. . 3 ⊢ (𝑠 = 𝑎 → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑎 ∩ 𝑡))))
6		fveq2 6885	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
7	6	ineq2d 4176	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
8		ineq2 4170	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
9	8	fveq2d 6889	. . . 4 ⊢ (𝑡 = 𝑏 → (𝐼‘(𝑎 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑏)))
10	7, 9	sseq12d 3973	. . 3 ⊢ (𝑡 = 𝑏 → (((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑎 ∩ 𝑡)) ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏))))
11	5, 10	cbvral2vw 3250	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)))
12		ntrcls.d	. . . . . 6 ⊢ 𝐷 = (𝑂‘𝐵)
13		ntrcls.r	. . . . . 6 ⊢ (𝜑 → 𝐼𝐷𝐾)
14	12, 13	ntrclsbex 44792	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
15		difssd 4094	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ⊆ 𝐵)
16	14, 15	sselpwd 5302	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18		elpwi 4572	. . . 4 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
19		simpl 488	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → 𝐵 ∈ V)
20		difssd 4094	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ⊆ 𝐵)
21	19, 20	sselpwd 5302	. . . . 5 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
22		simpr 490	. . . . . . . 8 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → 𝑠 = (𝐵 ∖ 𝑎))
23	22	difeq2d 4084	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
24	23	eqeq2d 2777	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
25		eqcom 2773	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
26	24, 25	bitrdi 290	. . . . 5 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎))
27		dfss4 4225	. . . . . 6 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
28	27	bilani 510	. . . . 5 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
29	21, 26, 28	rspcedvd 3586	. . . 4 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
30	14, 18, 29	syl2an 608	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
31		simpl1 1210	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝜑)
32		difssd 4094	. . . . . 6 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ⊆ 𝐵)
33	14, 32	sselpwd 5302	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
34	31, 33	syl 18	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
35		elpwi 4572	. . . . . 6 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
36		simpl 488	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → 𝐵 ∈ V)
37		difssd 4094	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ⊆ 𝐵)
38	36, 37	sselpwd 5302	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
39		simpr 490	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → 𝑡 = (𝐵 ∖ 𝑏))
40	39	difeq2d 4084	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
41	40	eqeq2d 2777	. . . . . . . 8 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
42		eqcom 2773	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
43	41, 42	bitrdi 290	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏))
44		dfss4 4225	. . . . . . . 8 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
45	44	bilani 510	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
46	38, 43, 45	rspcedvd 3586	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
47	14, 35, 46	syl2an 608	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
48	47	3ad2antl1 1204	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
49		simp13 1224	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑎 = (𝐵 ∖ 𝑠))
50		fveq2 6885	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
51	50	ineq1d 4175	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
52		ineq1 4169	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
53	52	fveq2d 6889	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘(𝑎 ∩ 𝑏)) = (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)))
54	51, 53	sseq12d 3973	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏))))
55	49, 54	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏))))
56		fveq2 6885	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
57	56	ineq2d 4176	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
58		ineq2 4170	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
59		difundi 4246	. . . . . . . . 9 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
60	58, 59	eqtr4di 2819	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠 ∪ 𝑡)))
61	60	fveq2d 6889	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))
62	57, 61	sseq12d 3973	. . . . . 6 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
63	62	3ad2ant3 1153	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
64		simp11 1222	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
65		ntrcls.o	. . . . . . . . 9 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
66	65, 12, 13	ntrclsiex 44811	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
67	66, 14	jca 521	. . . . . . 7 ⊢ (𝜑 → (𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V))
68		elmapi 8848	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
69	68	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
70		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → 𝐵 ∈ V)
71		difssd 4094	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
72	70, 71	sselpwd 5302	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
73	69, 72	ffvelcdmd 7084	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
74	73	elpwid 4574	. . . . . . . . 9 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
75		orc 881	. . . . . . . . 9 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ∨ (𝐼‘(𝐵 ∖ 𝑡)) ⊆ 𝐵))
76		inss 4204	. . . . . . . . 9 ⊢ (((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ∨ (𝐼‘(𝐵 ∖ 𝑡)) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
77	74, 75, 76	3syl 19	. . . . . . . 8 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
78		difssd 4094	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ⊆ 𝐵)
79	70, 78	sselpwd 5302	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ∈ 𝒫 𝐵)
80	69, 79	ffvelcdmd 7084	. . . . . . . . 9 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ∈ 𝒫 𝐵)
81	80	elpwid 4574	. . . . . . . 8 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵)
82	77, 81	jca 521	. . . . . . 7 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝐵 ∈ V) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵))
83		sscon34b 4260	. . . . . . 7 ⊢ ((((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
84	64, 67, 82, 83	4syl 20	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
85		difindi 4248	. . . . . . . 8 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
86	85	sseq2i 3969	. . . . . . 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 44551	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
92		simpl2 1211	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
93		simpl3 1212	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
94		eqid 2766	. . . . . . . . . 10 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
95		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
96		simprl 783	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
97	96	elpwid 4574	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ⊆ 𝐵)
98		simprr 785	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
99	98	elpwid 4574	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ⊆ 𝐵)
100	97, 99	unssd 4148	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
101	95, 100	sselpwd 5302	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵)
102	101	3ad2antl2 1205	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵)
103		eqid 2766	. . . . . . . . . 10 ⊢ ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡))
104	65, 12, 92, 93, 94, 102, 103	dssmapfv3d 44777	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
105		simpl1 1210	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝜑)
106	65, 12, 13	ntrclsfv1 44813	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
107	106	fveq1d 6887	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡)))
108	105, 107	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡)))
109	104, 108	eqtr3d 2803	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐾‘(𝑠 ∪ 𝑡)))
110		simprl 783	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
111		eqid 2766	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
112	65, 12, 92, 93, 94, 110, 111	dssmapfv3d 44777	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
113	106	fveq1d 6887	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
114	105, 113	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
115	112, 114	eqtr3d 2803	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) = (𝐾‘𝑠))
116		simprr 785	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
117		eqid 2766	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
118	65, 12, 92, 93, 94, 116, 117	dssmapfv3d 44777	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
119	106	fveq1d 6887	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
120	105, 119	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
121	118, 120	eqtr3d 2803	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))) = (𝐾‘𝑡))
122	115, 121	uneq12d 4126	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
123	109, 122	sseq12d 3973	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
124	64, 88, 89, 90, 91, 123	syl32anc 1405	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
125	84, 87, 124	3bitrd 308	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
126	55, 63, 125	3bitrd 308	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
127	34, 48, 126	ralxfrd2 5386	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
128	17, 30, 127	ralxfrd2 5386	. 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 2146 ∀wral 3082 ∃wrex 3092 Vcvv 3458 ∖ cdif 3905 ∪ cun 3906 ∩ cin 3907 ⊆ wss 3908 𝒫 cpw 4565 class class class wbr 5112 ↦ cmpt 5195 ⟶wf 6536 ‘cfv 6540 (class class class)co 7416 ↑_m cmap 8826

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 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5241 ax-sep 5260 ax-nul 5272 ax-pow 5339 ax-pr 5407 ax-un 7738 ax-frege1 44548

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 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4876 df-iun 4961 df-br 5113 df-opab 5177 df-mpt 5196 df-id 5559 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7419 df-oprab 7420 df-mpo 7421 df-1st 7988 df-2nd 7989 df-map 8828

This theorem is used by: (None)

W3C validator