ntrclsk3

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)

	Ref	Expression
Hypotheses	ntrcls.o	$⊢ O = (i \in V ⟼ (k \in ({𝒫 i}^{𝒫 i}) ⟼ (j \in 𝒫 i ⟼ i ∖ k (i ∖ j))))$
	ntrcls.d	$⊢ D = O (B)$
	ntrcls.r	$⊢ φ \to I D K$
Assertion	ntrclsk3	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B K (s \cup t) \subseteq K (s) \cup K (t))$

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	$⊢ O = (i \in V ⟼ (k \in ({𝒫 i}^{𝒫 i}) ⟼ (j \in 𝒫 i ⟼ i ∖ k (i ∖ j))))$
2		ntrcls.d	$⊢ D = O (B)$
3		ntrcls.r	$⊢ φ \to I D K$
4		fveq2	$⊢ s = a \to I (s) = I (a)$
5	4	ineq1d	$⊢ s = a \to I (s) \cap I (t) = I (a) \cap I (t)$
6		ineq1	$⊢ s = a \to s \cap t = a \cap t$
7	6	fveq2d	$⊢ s = a \to I (s \cap t) = I (a \cap t)$
8	5 7	sseq12d	$⊢ s = a \to (I (s) \cap I (t) \subseteq I (s \cap t) \leftrightarrow I (a) \cap I (t) \subseteq I (a \cap t))$
9		fveq2	$⊢ t = b \to I (t) = I (b)$
10	9	ineq2d	$⊢ t = b \to I (a) \cap I (t) = I (a) \cap I (b)$
11		ineq2	$⊢ t = b \to a \cap t = a \cap b$
12	11	fveq2d	$⊢ t = b \to I (a \cap t) = I (a \cap b)$
13	10 12	sseq12d	$⊢ t = b \to (I (a) \cap I (t) \subseteq I (a \cap t) \leftrightarrow I (a) \cap I (b) \subseteq I (a \cap b))$
14	8 13	cbvral2vw	$⊢ \forall s \in 𝒫 B \forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t) \leftrightarrow \forall a \in 𝒫 B \forall b \in 𝒫 B I (a) \cap I (b) \subseteq I (a \cap b)$
15	2 3	ntrclsbex	$⊢ φ \to B \in V$
16		difssd	$⊢ φ \to B ∖ s \subseteq B$
17	15 16	sselpwd	$⊢ φ \to B ∖ s \in 𝒫 B$
18	17	adantr	$⊢ (φ \land s \in 𝒫 B) \to B ∖ s \in 𝒫 B$
19		elpwi	$⊢ a \in 𝒫 B \to a \subseteq B$
20		simpl	$⊢ (B \in V \land a \subseteq B) \to B \in V$
21		difssd	$⊢ (B \in V \land a \subseteq B) \to B ∖ a \subseteq B$
22	20 21	sselpwd	$⊢ (B \in V \land a \subseteq B) \to B ∖ a \in 𝒫 B$
23		simpr	$⊢ ((B \in V \land a \subseteq B) \land s = B ∖ a) \to s = B ∖ a$
24	23	difeq2d	$⊢ ((B \in V \land a \subseteq B) \land s = B ∖ a) \to B ∖ s = B ∖ (B ∖ a)$
25	24	eqeq2d	$⊢ ((B \in V \land a \subseteq B) \land s = B ∖ a) \to (a = B ∖ s \leftrightarrow a = B ∖ (B ∖ a))$
26		eqcom	$⊢ a = B ∖ (B ∖ a) \leftrightarrow B ∖ (B ∖ a) = a$
27	25 26	bitrdi	$⊢ ((B \in V \land a \subseteq B) \land s = B ∖ a) \to (a = B ∖ s \leftrightarrow B ∖ (B ∖ a) = a)$
28		dfss4	$⊢ a \subseteq B \leftrightarrow B ∖ (B ∖ a) = a$
29	28	biimpi	$⊢ a \subseteq B \to B ∖ (B ∖ a) = a$
30	29	adantl	$⊢ (B \in V \land a \subseteq B) \to B ∖ (B ∖ a) = a$
31	22 27 30	rspcedvd	$⊢ (B \in V \land a \subseteq B) \to \exists s \in 𝒫 B a = B ∖ s$
32	15 19 31	syl2an	$⊢ (φ \land a \in 𝒫 B) \to \exists s \in 𝒫 B a = B ∖ s$
33		simpl1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to φ$
34		difssd	$⊢ φ \to B ∖ t \subseteq B$
35	15 34	sselpwd	$⊢ φ \to B ∖ t \in 𝒫 B$
36	33 35	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to B ∖ t \in 𝒫 B$
37		elpwi	$⊢ b \in 𝒫 B \to b \subseteq B$
38		simpl	$⊢ (B \in V \land b \subseteq B) \to B \in V$
39		difssd	$⊢ (B \in V \land b \subseteq B) \to B ∖ b \subseteq B$
40	38 39	sselpwd	$⊢ (B \in V \land b \subseteq B) \to B ∖ b \in 𝒫 B$
41		simpr	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to t = B ∖ b$
42	41	difeq2d	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to B ∖ t = B ∖ (B ∖ b)$
43	42	eqeq2d	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to (b = B ∖ t \leftrightarrow b = B ∖ (B ∖ b))$
44		eqcom	$⊢ b = B ∖ (B ∖ b) \leftrightarrow B ∖ (B ∖ b) = b$
45	43 44	bitrdi	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to (b = B ∖ t \leftrightarrow B ∖ (B ∖ b) = b)$
46		dfss4	$⊢ b \subseteq B \leftrightarrow B ∖ (B ∖ b) = b$
47	46	biimpi	$⊢ b \subseteq B \to B ∖ (B ∖ b) = b$
48	47	adantl	$⊢ (B \in V \land b \subseteq B) \to B ∖ (B ∖ b) = b$
49	40 45 48	rspcedvd	$⊢ (B \in V \land b \subseteq B) \to \exists t \in 𝒫 B b = B ∖ t$
50	15 37 49	syl2an	$⊢ (φ \land b \in 𝒫 B) \to \exists t \in 𝒫 B b = B ∖ t$
51	50	3ad2antl1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land b \in 𝒫 B) \to \exists t \in 𝒫 B b = B ∖ t$
52		simp13	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to a = B ∖ s$
53		fveq2	$⊢ a = B ∖ s \to I (a) = I (B ∖ s)$
54	53	ineq1d	$⊢ a = B ∖ s \to I (a) \cap I (b) = I (B ∖ s) \cap I (b)$
55		ineq1	$⊢ a = B ∖ s \to a \cap b = (B ∖ s) \cap b$
56	55	fveq2d	$⊢ a = B ∖ s \to I (a \cap b) = I ((B ∖ s) \cap b)$
57	54 56	sseq12d	$⊢ a = B ∖ s \to (I (a) \cap I (b) \subseteq I (a \cap b) \leftrightarrow I (B ∖ s) \cap I (b) \subseteq I ((B ∖ s) \cap b))$
58	52 57	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (I (a) \cap I (b) \subseteq I (a \cap b) \leftrightarrow I (B ∖ s) \cap I (b) \subseteq I ((B ∖ s) \cap b))$
59		fveq2	$⊢ b = B ∖ t \to I (b) = I (B ∖ t)$
60	59	ineq2d	$⊢ b = B ∖ t \to I (B ∖ s) \cap I (b) = I (B ∖ s) \cap I (B ∖ t)$
61		ineq2	$⊢ b = B ∖ t \to (B ∖ s) \cap b = (B ∖ s) \cap (B ∖ t)$
62		difundi	$⊢ B ∖ (s \cup t) = (B ∖ s) \cap (B ∖ t)$
63	61 62	eqtr4di	$⊢ b = B ∖ t \to (B ∖ s) \cap b = B ∖ (s \cup t)$
64	63	fveq2d	$⊢ b = B ∖ t \to I ((B ∖ s) \cap b) = I (B ∖ (s \cup t))$
65	60 64	sseq12d	$⊢ b = B ∖ t \to (I (B ∖ s) \cap I (b) \subseteq I ((B ∖ s) \cap b) \leftrightarrow I (B ∖ s) \cap I (B ∖ t) \subseteq I (B ∖ (s \cup t)))$
66	65	3ad2ant3	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (I (B ∖ s) \cap I (b) \subseteq I ((B ∖ s) \cap b) \leftrightarrow I (B ∖ s) \cap I (B ∖ t) \subseteq I (B ∖ (s \cup t)))$
67		simp11	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to φ$
68	1 2 3	ntrclsiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
69	68 15	jca	$⊢ φ \to (I \in ({𝒫 B}^{𝒫 B}) \land B \in V)$
70	67 69	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (I \in ({𝒫 B}^{𝒫 B}) \land B \in V)$
71		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
72	71	adantr	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I : 𝒫 B ⟶ 𝒫 B$
73		simpr	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B \in V$
74		difssd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ s \subseteq B$
75	73 74	sselpwd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ s \in 𝒫 B$
76	72 75	ffvelrnd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ s) \in 𝒫 B$
77	76	elpwid	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ s) \subseteq B$
78		orc	$⊢ I (B ∖ s) \subseteq B \to (I (B ∖ s) \subseteq B \lor I (B ∖ t) \subseteq B)$
79		inss	$⊢ (I (B ∖ s) \subseteq B \lor I (B ∖ t) \subseteq B) \to I (B ∖ s) \cap I (B ∖ t) \subseteq B$
80	77 78 79	3syl	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ s) \cap I (B ∖ t) \subseteq B$
81		difssd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ (s \cup t) \subseteq B$
82	73 81	sselpwd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ (s \cup t) \in 𝒫 B$
83	72 82	ffvelrnd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ (s \cup t)) \in 𝒫 B$
84	83	elpwid	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ (s \cup t)) \subseteq B$
85	80 84	jca	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to (I (B ∖ s) \cap I (B ∖ t) \subseteq B \land I (B ∖ (s \cup t)) \subseteq B)$
86		sscon34b	$⊢ (I (B ∖ s) \cap I (B ∖ t) \subseteq B \land I (B ∖ (s \cup t)) \subseteq B) \to (I (B ∖ s) \cap I (B ∖ t) \subseteq I (B ∖ (s \cup t)) \leftrightarrow B ∖ I (B ∖ (s \cup t)) \subseteq B ∖ (I (B ∖ s) \cap I (B ∖ t)))$
87	70 85 86	3syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (I (B ∖ s) \cap I (B ∖ t) \subseteq I (B ∖ (s \cup t)) \leftrightarrow B ∖ I (B ∖ (s \cup t)) \subseteq B ∖ (I (B ∖ s) \cap I (B ∖ t)))$
88		difindi	$⊢ B ∖ (I (B ∖ s) \cap I (B ∖ t)) = (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t))$
89	88	sseq2i	$⊢ B ∖ I (B ∖ (s \cup t)) \subseteq B ∖ (I (B ∖ s) \cap I (B ∖ t)) \leftrightarrow B ∖ I (B ∖ (s \cup t)) \subseteq (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t))$
90	89	a1i	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (B ∖ I (B ∖ (s \cup t)) \subseteq B ∖ (I (B ∖ s) \cap I (B ∖ t)) \leftrightarrow B ∖ I (B ∖ (s \cup t)) \subseteq (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t)))$
91	67 15	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B \in V$
92	67 68	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I \in ({𝒫 B}^{𝒫 B})$
93		simp12	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to s \in 𝒫 B$
94		rp-simp2	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to t \in 𝒫 B$
95		simpl2	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to B \in V$
96		simpl3	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to I \in ({𝒫 B}^{𝒫 B})$
97		eqid	$⊢ D (I) = D (I)$
98		simpl	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to B \in V$
99		simprl	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \in 𝒫 B$
100	99	elpwid	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \subseteq B$
101		simprr	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to t \in 𝒫 B$
102	101	elpwid	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to t \subseteq B$
103	100 102	unssd	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \cup t \subseteq B$
104	98 103	sselpwd	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \cup t \in 𝒫 B$
105	104	3ad2antl2	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \cup t \in 𝒫 B$
106		eqid	$⊢ D (I) (s \cup t) = D (I) (s \cup t)$
107	1 2 95 96 97 105 106	dssmapfv3d	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (s \cup t) = B ∖ I (B ∖ (s \cup t))$
108		simpl1	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to φ$
109	1 2 3	ntrclsfv1	$⊢ φ \to D (I) = K$
110	109	fveq1d	$⊢ φ \to D (I) (s \cup t) = K (s \cup t)$
111	108 110	syl	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (s \cup t) = K (s \cup t)$
112	107 111	eqtr3d	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to B ∖ I (B ∖ (s \cup t)) = K (s \cup t)$
113		simprl	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \in 𝒫 B$
114		eqid	$⊢ D (I) (s) = D (I) (s)$
115	1 2 95 96 97 113 114	dssmapfv3d	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (s) = B ∖ I (B ∖ s)$
116	109	fveq1d	$⊢ φ \to D (I) (s) = K (s)$
117	108 116	syl	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (s) = K (s)$
118	115 117	eqtr3d	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to B ∖ I (B ∖ s) = K (s)$
119		simprr	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to t \in 𝒫 B$
120		eqid	$⊢ D (I) (t) = D (I) (t)$
121	1 2 95 96 97 119 120	dssmapfv3d	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (t) = B ∖ I (B ∖ t)$
122	109	fveq1d	$⊢ φ \to D (I) (t) = K (t)$
123	108 122	syl	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (t) = K (t)$
124	121 123	eqtr3d	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to B ∖ I (B ∖ t) = K (t)$
125	118 124	uneq12d	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t)) = K (s) \cup K (t)$
126	112 125	sseq12d	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to (B ∖ I (B ∖ (s \cup t)) \subseteq (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t)) \leftrightarrow K (s \cup t) \subseteq K (s) \cup K (t))$
127	67 91 92 93 94 126	syl32anc	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (B ∖ I (B ∖ (s \cup t)) \subseteq (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t)) \leftrightarrow K (s \cup t) \subseteq K (s) \cup K (t))$
128	87 90 127	3bitrd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (I (B ∖ s) \cap I (B ∖ t) \subseteq I (B ∖ (s \cup t)) \leftrightarrow K (s \cup t) \subseteq K (s) \cup K (t))$
129	58 66 128	3bitrd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (I (a) \cap I (b) \subseteq I (a \cap b) \leftrightarrow K (s \cup t) \subseteq K (s) \cup K (t))$
130	36 51 129	ralxfrd2	$⊢ (φ \land s \in 𝒫 B \land a = B ∖ s) \to (\forall b \in 𝒫 B I (a) \cap I (b) \subseteq I (a \cap b) \leftrightarrow \forall t \in 𝒫 B K (s \cup t) \subseteq K (s) \cup K (t))$
131	18 32 130	ralxfrd2	$⊢ φ \to (\forall a \in 𝒫 B \forall b \in 𝒫 B I (a) \cap I (b) \subseteq I (a \cap b) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B K (s \cup t) \subseteq K (s) \cup K (t))$
132	14 131	syl5bb	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B K (s \cup t) \subseteq K (s) \cup K (t))$

Metamath Proof Explorer

Theorem ntrclsk3

Proof