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	bilani	$⊢ (B \in V \land a \subseteq B) \to B ∖ (B ∖ a) = a$
30	22 27 29	rspcedvd	$⊢ (B \in V \land a \subseteq B) \to \exists s \in 𝒫 B a = B ∖ s$
31	15 19 30	syl2an	$⊢ (φ \land a \in 𝒫 B) \to \exists s \in 𝒫 B a = B ∖ s$
32		simpl1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to φ$
33		difssd	$⊢ φ \to B ∖ t \subseteq B$
34	15 33	sselpwd	$⊢ φ \to B ∖ t \in 𝒫 B$
35	32 34	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to B ∖ t \in 𝒫 B$
36		elpwi	$⊢ b \in 𝒫 B \to b \subseteq B$
37		simpl	$⊢ (B \in V \land b \subseteq B) \to B \in V$
38		difssd	$⊢ (B \in V \land b \subseteq B) \to B ∖ b \subseteq B$
39	37 38	sselpwd	$⊢ (B \in V \land b \subseteq B) \to B ∖ b \in 𝒫 B$
40		simpr	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to t = B ∖ b$
41	40	difeq2d	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to B ∖ t = B ∖ (B ∖ b)$
42	41	eqeq2d	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to (b = B ∖ t \leftrightarrow b = B ∖ (B ∖ b))$
43		eqcom	$⊢ b = B ∖ (B ∖ b) \leftrightarrow B ∖ (B ∖ b) = b$
44	42 43	bitrdi	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to (b = B ∖ t \leftrightarrow B ∖ (B ∖ b) = b)$
45		dfss4	$⊢ b \subseteq B \leftrightarrow B ∖ (B ∖ b) = b$
46	45	bilani	$⊢ (B \in V \land b \subseteq B) \to B ∖ (B ∖ b) = b$
47	39 44 46	rspcedvd	$⊢ (B \in V \land b \subseteq B) \to \exists t \in 𝒫 B b = B ∖ t$
48	15 36 47	syl2an	$⊢ (φ \land b \in 𝒫 B) \to \exists t \in 𝒫 B b = B ∖ t$
49	48	3ad2antl1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land b \in 𝒫 B) \to \exists t \in 𝒫 B b = B ∖ t$
50		simp13	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to a = B ∖ s$
51		fveq2	$⊢ a = B ∖ s \to I (a) = I (B ∖ s)$
52	51	ineq1d	$⊢ a = B ∖ s \to I (a) \cap I (b) = I (B ∖ s) \cap I (b)$
53		ineq1	$⊢ a = B ∖ s \to a \cap b = (B ∖ s) \cap b$
54	53	fveq2d	$⊢ a = B ∖ s \to I (a \cap b) = I ((B ∖ s) \cap b)$
55	52 54	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))$
56	50 55	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))$
57		fveq2	$⊢ b = B ∖ t \to I (b) = I (B ∖ t)$
58	57	ineq2d	$⊢ b = B ∖ t \to I (B ∖ s) \cap I (b) = I (B ∖ s) \cap I (B ∖ t)$
59		ineq2	$⊢ b = B ∖ t \to (B ∖ s) \cap b = (B ∖ s) \cap (B ∖ t)$
60		difundi	$⊢ B ∖ (s \cup t) = (B ∖ s) \cap (B ∖ t)$
61	59 60	eqtr4di	$⊢ b = B ∖ t \to (B ∖ s) \cap b = B ∖ (s \cup t)$
62	61	fveq2d	$⊢ b = B ∖ t \to I ((B ∖ s) \cap b) = I (B ∖ (s \cup t))$
63	58 62	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)))$
64	63	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)))$
65		simp11	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to φ$
66	1 2 3	ntrclsiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
67	66 15	jca	$⊢ φ \to (I \in ({𝒫 B}^{𝒫 B}) \land B \in V)$
68		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
69	68	adantr	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I : 𝒫 B ⟶ 𝒫 B$
70		simpr	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B \in V$
71		difssd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ s \subseteq B$
72	70 71	sselpwd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ s \in 𝒫 B$
73	69 72	ffvelcdmd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ s) \in 𝒫 B$
74	73	elpwid	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ s) \subseteq B$
75		orc	$⊢ I (B ∖ s) \subseteq B \to (I (B ∖ s) \subseteq B \lor I (B ∖ t) \subseteq B)$
76		inss	$⊢ (I (B ∖ s) \subseteq B \lor I (B ∖ t) \subseteq B) \to I (B ∖ s) \cap I (B ∖ t) \subseteq B$
77	74 75 76	3syl	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ s) \cap I (B ∖ t) \subseteq B$
78		difssd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ (s \cup t) \subseteq B$
79	70 78	sselpwd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to B ∖ (s \cup t) \in 𝒫 B$
80	69 79	ffvelcdmd	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ (s \cup t)) \in 𝒫 B$
81	80	elpwid	$⊢ (I \in ({𝒫 B}^{𝒫 B}) \land B \in V) \to I (B ∖ (s \cup t)) \subseteq B$
82	77 81	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)$
83		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)))$
84	65 67 82 83	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)))$
85		difindi	$⊢ B ∖ (I (B ∖ s) \cap I (B ∖ t)) = (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t))$
86	85	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))$
87	86	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)))$
88	65 15	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B \in V$
89	65 66	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I \in ({𝒫 B}^{𝒫 B})$
90		simp12	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to s \in 𝒫 B$
91		rp-simp2	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to t \in 𝒫 B$
92		simpl2	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to B \in V$
93		simpl3	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to I \in ({𝒫 B}^{𝒫 B})$
94		eqid	$⊢ D (I) = D (I)$
95		simpl	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to B \in V$
96		simprl	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \in 𝒫 B$
97	96	elpwid	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \subseteq B$
98		simprr	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to t \in 𝒫 B$
99	98	elpwid	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to t \subseteq B$
100	97 99	unssd	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \cup t \subseteq B$
101	95 100	sselpwd	$⊢ (B \in V \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \cup t \in 𝒫 B$
102	101	3ad2antl2	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \cup t \in 𝒫 B$
103		eqid	$⊢ D (I) (s \cup t) = D (I) (s \cup t)$
104	1 2 92 93 94 102 103	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))$
105		simpl1	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to φ$
106	1 2 3	ntrclsfv1	$⊢ φ \to D (I) = K$
107	106	fveq1d	$⊢ φ \to D (I) (s \cup t) = K (s \cup t)$
108	105 107	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)$
109	104 108	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)$
110		simprl	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \in 𝒫 B$
111		eqid	$⊢ D (I) (s) = D (I) (s)$
112	1 2 92 93 94 110 111	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)$
113	106	fveq1d	$⊢ φ \to D (I) (s) = K (s)$
114	105 113	syl	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (s) = K (s)$
115	112 114	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)$
116		simprr	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to t \in 𝒫 B$
117		eqid	$⊢ D (I) (t) = D (I) (t)$
118	1 2 92 93 94 116 117	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)$
119	106	fveq1d	$⊢ φ \to D (I) (t) = K (t)$
120	105 119	syl	$⊢ ((φ \land B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (t) = K (t)$
121	118 120	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)$
122	115 121	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)$
123	109 122	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))$
124	65 88 89 90 91 123	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))$
125	84 87 124	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))$
126	56 64 125	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))$
127	35 49 126	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))$
128	18 31 127	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))$
129	14 128	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