Theorem ntrclsk13 40774

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 4131	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
2	1	fveq2d 6649	. . . 4 ⊢ (𝑠 = 𝑎 → (𝐼‘(𝑠 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑡)))
3		fveq2 6645	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
4	3	ineq1d 4138	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
5	2, 4	eqeq12d 2814	. . 3 ⊢ (𝑠 = 𝑎 → ((𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ (𝐼‘(𝑎 ∩ 𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡))))
6		ineq2 4133	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
7	6	fveq2d 6649	. . . 4 ⊢ (𝑡 = 𝑏 → (𝐼‘(𝑎 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑏)))
8		fveq2 6645	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
9	8	ineq2d 4139	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
10	7, 9	eqeq12d 2814	. . 3 ⊢ (𝑡 = 𝑏 → ((𝐼‘(𝑎 ∩ 𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ↔ (𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏))))
11	5, 10	cbvral2vw 3408	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
12		ntrcls.d	. . . . . 6 ⊢ 𝐷 = (𝑂‘𝐵)
13		ntrcls.r	. . . . . 6 ⊢ (𝜑 → 𝐼𝐷𝐾)
14	12, 13	ntrclsbex 40737	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
15		difssd 4060	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ⊆ 𝐵)
16	14, 15	sselpwd 5194	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 484	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18		elpwi 4506	. . . 4 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
19	14	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → 𝐵 ∈ V)
20		difssd 4060	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ⊆ 𝐵)
21	19, 20	sselpwd 5194	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
22		difeq2 4044	. . . . . . . 8 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
23	22	eqeq2d 2809	. . . . . . 7 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
24		eqcom 2805	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
25	23, 24	syl6bb 290	. . . . . 6 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎))
26	25	adantl 485	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎))
27		dfss4 4185	. . . . . . 7 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
28	27	biimpi 219	. . . . . 6 ⊢ (𝑎 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
29	28	adantl 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
30	21, 26, 29	rspcedvd 3574	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
31	18, 30	sylan2 595	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
32		ineq1 4131	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
33	32	fveq2d 6649	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘(𝑎 ∩ 𝑏)) = (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)))
34		fveq2 6645	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
35	34	ineq1d 4138	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
36	33, 35	eqeq12d 2814	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
37	36	ralbidv 3162	. . . . 5 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
38	37	3ad2ant3 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
39		difssd 4060	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ⊆ 𝐵)
40	14, 39	sselpwd 5194	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
41	40	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
42		simpll 766	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝜑)
43		elpwi 4506	. . . . . . . 8 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
44	43	adantl 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏 ⊆ 𝐵)
45		difssd 4060	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ⊆ 𝐵)
46	14, 45	sselpwd 5194	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
47	46	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
48		difeq2 4044	. . . . . . . . . . 11 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
49	48	eqeq2d 2809	. . . . . . . . . 10 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
50		eqcom 2805	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
51	49, 50	syl6bb 290	. . . . . . . . 9 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏))
52	51	adantl 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏))
53		dfss4 4185	. . . . . . . . . 10 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
54	53	biimpi 219	. . . . . . . . 9 ⊢ (𝑏 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
55	54	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
56	47, 52, 55	rspcedvd 3574	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
57	42, 44, 56	syl2anc 587	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
58		ineq2 4133	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
59		difundi 4206	. . . . . . . . . . 11 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
60	58, 59	eqtr4di 2851	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠 ∪ 𝑡)))
61	60	fveq2d 6649	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))
62		fveq2 6645	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
63	62	ineq2d 4139	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
64	61, 63	eqeq12d 2814	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
65	64	3ad2ant3 1132	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
66		simp1l 1194	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
67	66, 14	jccir 525	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (𝜑 ∧ 𝐵 ∈ V))
68		simp1r 1195	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
69		simp2 1134	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
70		ntrcls.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
71	70, 12, 13	ntrclsiex 40756	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵))
72		elmapi 8411	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
73	71, 72	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
74	73	anim1i 617	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ∈ V) → (𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V))
75	74	adantr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V))
76		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
77		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → 𝐵 ∈ V)
78		difssd 4060	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ⊆ 𝐵)
79	77, 78	sselpwd 5194	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ∈ 𝒫 𝐵)
80	76, 79	ffvelrnd 6829	. . . . . . . . . . . 12 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ∈ 𝒫 𝐵)
81	80	elpwid 4508	. . . . . . . . . . 11 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵)
82		difssd 4060	. . . . . . . . . . . . . . 15 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
83	77, 82	sselpwd 5194	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
84	76, 83	ffvelrnd 6829	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
85	84	elpwid 4508	. . . . . . . . . . . 12 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
86		ssinss1 4164	. . . . . . . . . . . 12 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
87	85, 86	syl 17	. . . . . . . . . . 11 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
88	81, 87	jca 515	. . . . . . . . . 10 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵))
89		rcompleq 4220	. . . . . . . . . 10 ⊢ (((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
90	75, 88, 89	3syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
91		simplr 768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
92	71	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵))
93		eqid 2798	. . . . . . . . . . 11 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
94		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
95	94	elpwid 4508	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ⊆ 𝐵)
96		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
97	96	elpwid 4508	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ⊆ 𝐵)
98	95, 97	unssd 4113	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
99	91, 98	sselpwd 5194	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵)
100		eqid 2798	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡))
101	70, 12, 91, 92, 93, 99, 100	dssmapfv3d 40720	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
102		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
103		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
104	71	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵))
105		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
106		eqid 2798	. . . . . . . . . . . . . 14 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
107	70, 12, 103, 104, 93, 105, 106	dssmapfv3d 40720	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
108	102, 107	sylan2 595	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
109		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
110		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
111	71	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵))
112		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
113		eqid 2798	. . . . . . . . . . . . . 14 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
114	70, 12, 110, 111, 93, 112, 113	dssmapfv3d 40720	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
115	109, 114	sylan2 595	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
116	108, 115	uneq12d 4091	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))
117		difindi 4208	. . . . . . . . . . 11 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
118	116, 117	eqtr4di 2851	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
119	101, 118	eqeq12d 2814	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
120		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝜑)
121	70, 12, 13	ntrclsfv1 40758	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
122		fveq1 6644	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡)))
123		fveq1 6644	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
124		fveq1 6644	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
125	123, 124	uneq12d 4091	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
126	122, 125	eqeq12d 2814	. . . . . . . . . 10 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
127	120, 121, 126	3syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
128	90, 119, 127	3bitr2d 310	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
129	67, 68, 69, 128	syl12anc 835	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
130	65, 129	bitrd 282	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
131	41, 57, 130	ralxfrd2 5278	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
132	131	3adant3 1129	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
133	38, 132	bitrd 282	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
134	17, 31, 133	ralxfrd2 5278	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
135	11, 134	syl5bb 286	1 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  𝒫 cpw 4497   class class class wbr 5030   ↦ cmpt 5110  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135   ↑_m cmap 8389

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-map 8391

This theorem is referenced by: (None)