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		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
71	70	adantr	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I : 𝒫 B ⟶ 𝒫 B$
72		simpr	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B \in V$
73		difssd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ s \subseteq B$
74	72 73	sselpwd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ s \in 𝒫 B$
75	71 74	ffvelcdmd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ s) \in 𝒫 B$
76	75	elpwid	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ s) \subseteq B$
77		orc	$⊢ I (B ∖ s) \subseteq B \to (I (B ∖ s) \subseteq B \lor I (B ∖ t) \subseteq B)$
78		inss	$⊢ (I (B ∖ s) \subseteq B \lor I (B ∖ t) \subseteq B) \to I (B ∖ s) \cap I (B ∖ t) \subseteq B$
79	76 77 78	3syl	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ s) \cap I (B ∖ t) \subseteq B$
80		difssd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ (s \cup t) \subseteq B$
81	72 80	sselpwd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ (s \cup t) \in 𝒫 B$
82	71 81	ffvelcdmd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ (s \cup t)) \in 𝒫 B$
83	82	elpwid	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ (s \cup t)) \subseteq B$
84	79 83	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)$
85		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)))$
86	67 69 84 85	4syl	$⊢ ((φ \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)))$
87		difindi	$⊢ B ∖ (I (B ∖ s) \cap I (B ∖ t)) = (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t))$
88	87	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))$
89	88	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)))$
90	67 15	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B \in V$
91	67 68	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I \in ({𝒫 B}^{𝒫 B})$
92		simp12	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to s \in 𝒫 B$
93		rp-simp2	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to t \in 𝒫 B$
94		simpl2	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to B \in V$
95		simpl3	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to I \in ({𝒫 B}^{𝒫 B})$
96		eqid	$⊢ D (I) = D (I)$
97		simpl	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to B \in V$
98		simprl	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \in 𝒫 B$
99	98	elpwid	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \subseteq B$
100		simprr	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to t \in 𝒫 B$
101	100	elpwid	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to t \subseteq B$
102	99 101	unssd	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \cup t \subseteq B$
103	97 102	sselpwd	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \cup t \in 𝒫 B$
104	103	3ad2antl2	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \cup t \in 𝒫 B$
105		eqid	$⊢ D (I) (s \cup t) = D (I) (s \cup t)$
106	1 2 94 95 96 104 105	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))$
107		simpl1	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to φ$
108	1 2 3	ntrclsfv1	$⊢ φ \to D (I) = K$
109	108	fveq1d	$⊢ φ \to D (I) (s \cup t) = K (s \cup t)$
110	107 109	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)$
111	106 110	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)$
112		simprl	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \in 𝒫 B$
113		eqid	$⊢ D (I) (s) = D (I) (s)$
114	1 2 94 95 96 112 113	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)$
115	108	fveq1d	$⊢ φ \to D (I) (s) = K (s)$
116	107 115	syl	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (s) = K (s)$
117	114 116	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)$
118		simprr	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to t \in 𝒫 B$
119		eqid	$⊢ D (I) (t) = D (I) (t)$
120	1 2 94 95 96 118 119	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)$
121	108	fveq1d	$⊢ φ \to D (I) (t) = K (t)$
122	107 121	syl	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (t) = K (t)$
123	120 122	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)$
124	117 123	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)$
125	111 124	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))$
126	67 90 91 92 93 125	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))$
127	86 89 126	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))$
128	58 66 127	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))$
129	36 51 128	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))$
130	18 32 129	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))$
131	14 130	bitrid	$⊢ φ \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