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 45114

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 4110	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
2	1	fveq2d 6889	. . . 4 ⊢ (𝑠 = 𝑎 → (𝐼‘(𝑠 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑡)))
3		fveq2 6885	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
4	3	ineq1d 4116	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
5	2, 4	eqeq12d 2776	. . 3 ⊢ (𝑠 = 𝑎 → ((𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ (𝐼‘(𝑎 ∩ 𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡))))
6		ineq2 4111	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
7	6	fveq2d 6889	. . . 4 ⊢ (𝑡 = 𝑏 → (𝐼‘(𝑎 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑏)))
8		fveq2 6885	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
9	8	ineq2d 4117	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
10	7, 9	eqeq12d 2776	. . 3 ⊢ (𝑡 = 𝑏 → ((𝐼‘(𝑎 ∩ 𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ↔ (𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏))))
11	5, 10	cbvral2vw 3244	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
12		ntrcls.d	. . . . . 6 ⊢ 𝐷 = (𝑂‘𝐵)
13		ntrcls.r	. . . . . 6 ⊢ (𝜑 → 𝐼𝐷𝐾)
14	12, 13	ntrclsbex 45077	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
15		difssd 4073	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ⊆ 𝐵)
16	14, 15	sselpwd 5289	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18		elpwi 4563	. . . 4 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
19	14	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → 𝐵 ∈ V)
20		difssd 4073	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ⊆ 𝐵)
21	19, 20	sselpwd 5289	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
22		difeq2 4057	. . . . . . . 8 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
23	22	eqeq2d 2771	. . . . . . 7 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
24		eqcom 2767	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
25	23, 24	bitrdi 290	. . . . . 6 ⊢ (𝑠 = (𝐵 ∖ 𝑎) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎))
26	25	adantl 487	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎))
27		dfss4 4214	. . . . . 6 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
28	27	bilani 510	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
29	21, 26, 28	rspcedvd 3578	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
30	18, 29	sylan2 605	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
31		ineq1 4110	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
32	31	fveq2d 6889	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘(𝑎 ∩ 𝑏)) = (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)))
33		fveq2 6885	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
34	33	ineq1d 4116	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
35	32, 34	eqeq12d 2776	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
36	35	ralbidv 3185	. . . . 5 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
37	36	3ad2ant3 1153	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))))
38		difssd 4073	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ⊆ 𝐵)
39	14, 38	sselpwd 5289	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
40	39	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
41		simpll 779	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝜑)
42		elpwi 4563	. . . . . . . 8 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
43	42	adantl 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → 𝑏 ⊆ 𝐵)
44		difssd 4073	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ⊆ 𝐵)
45	14, 44	sselpwd 5289	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
46	45	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
47		difeq2 4057	. . . . . . . . . . 11 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
48	47	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
49		eqcom 2767	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
50	48, 49	bitrdi 290	. . . . . . . . 9 ⊢ (𝑡 = (𝐵 ∖ 𝑏) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏))
51	50	adantl 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏))
52		dfss4 4214	. . . . . . . . 9 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
53	52	bilani 510	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
54	46, 51, 53	rspcedvd 3578	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
55	41, 43, 54	syl2anc 596	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
56		ineq2 4111	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
57		difundi 4235	. . . . . . . . . . 11 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
58	56, 57	eqtr4di 2813	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠 ∪ 𝑡)))
59	58	fveq2d 6889	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))
60		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
61	60	ineq2d 4117	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
62	59, 61	eqeq12d 2776	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
63	62	3ad2ant3 1153	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
64		simp1l 1216	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
65	64, 14	jccir 531	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (𝜑 ∧ 𝐵 ∈ V))
66		simp1r 1217	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
67		simp2 1155	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
68		ntrcls.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
69	68, 12, 13	ntrclsiex 45096	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
70		elmapi 8869	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
71	69, 70	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
72	71	anim1i 627	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ∈ V) → (𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V))
73	72	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V))
74		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
75		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → 𝐵 ∈ V)
76		difssd 4073	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ⊆ 𝐵)
77	75, 76	sselpwd 5289	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ∈ 𝒫 𝐵)
78	74, 77	ffvelcdmd 7085	. . . . . . . . . . . 12 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ∈ 𝒫 𝐵)
79	78	elpwid 4565	. . . . . . . . . . 11 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵)
80		difssd 4073	. . . . . . . . . . . . . . 15 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
81	75, 80	sselpwd 5289	. . . . . . . . . . . . . 14 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
82	74, 81	ffvelcdmd 7085	. . . . . . . . . . . . 13 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
83	82	elpwid 4565	. . . . . . . . . . . 12 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
84		ssinss1 4142	. . . . . . . . . . . 12 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
85	83, 84	syl 18	. . . . . . . . . . 11 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
86	79, 85	jca 521	. . . . . . . . . 10 ⊢ ((𝐼:𝒫 𝐵⟶𝒫 𝐵 ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵))
87		rcompleq 4250	. . . . . . . . . 10 ⊢ (((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵 ∧ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
88	73, 86, 87	3syl 19	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
89		simplr 781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
90	69	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
91		eqid 2760	. . . . . . . . . . 11 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
92		simprl 783	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
93	92	elpwid 4565	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ⊆ 𝐵)
94		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
95	94	elpwid 4565	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ⊆ 𝐵)
96	93, 95	unssd 4190	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
97	89, 96	sselpwd 5289	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵)
98		eqid 2760	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡))
99	68, 12, 89, 90, 91, 97, 98	dssmapfv3d 45062	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
100		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
101		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
102	69	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
103		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵)
104		eqid 2760	. . . . . . . . . . . . . 14 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
105	68, 12, 101, 102, 91, 103, 104	dssmapfv3d 45062	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑠 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
106	100, 105	sylan2 605	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
107		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
108		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V)
109	69	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
110		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 ∈ 𝒫 𝐵)
111		eqid 2760	. . . . . . . . . . . . . 14 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
112	68, 12, 108, 109, 91, 110, 111	dssmapfv3d 45062	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
113	107, 112	sylan2 605	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
114	106, 113	uneq12d 4168	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))
115		difindi 4237	. . . . . . . . . . 11 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
116	114, 115	eqtr4di 2813	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))
117	99, 116	eqeq12d 2776	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
118		simpll 779	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝜑)
119	68, 12, 13	ntrclsfv1 45098	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
120		fveq1 6884	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡)))
121		fveq1 6884	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
122		fveq1 6884	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝐼) = 𝐾 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
123	121, 122	uneq12d 4168	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
124	120, 123	eqeq12d 2776	. . . . . . . . . 10 ⊢ ((𝐷‘𝐼) = 𝐾 → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
125	118, 119, 124	3syl 19	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (((𝐷‘𝐼)‘𝑠) ∪ ((𝐷‘𝐼)‘𝑡)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
126	88, 117, 125	3bitr2d 310	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ∈ V) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
127	65, 66, 67, 126	syl12anc 850	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
128	63, 127	bitrd 282	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
129	40, 55, 128	ralxfrd2 5373	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
130	129	3adant3 1150	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
131	37, 130	bitrd 282	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
132	17, 30, 131	ralxfrd2 5373	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵(𝐼‘(𝑎 ∩ 𝑏)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
133	11, 132	bitrid 286	1 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ⊆ wss 3895 ∖ cdif 4045 ∩ cin 4089 ∪ cun 4149 𝒫 cpw 4556 class class class wbr 5102 ↦ cmpt 5185 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ↑_m cmap 8847

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7423 df-oprab 7424 df-mpo 7425 df-1st 8001 df-2nd 8002 df-map 8849

This theorem is used by: (None)

W3C validator