ntrclsk13

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)

	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	ntrclsk13	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cap t) = I (s) \cap I (t) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B K (s \cup t) = 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		ineq1	$⊢ s = a \to s \cap t = a \cap t$
5	4	fveq2d	$⊢ s = a \to I (s \cap t) = I (a \cap t)$
6		fveq2	$⊢ s = a \to I (s) = I (a)$
7	6	ineq1d	$⊢ s = a \to I (s) \cap I (t) = I (a) \cap I (t)$
8	5 7	eqeq12d	$⊢ s = a \to (I (s \cap t) = I (s) \cap I (t) \leftrightarrow I (a \cap t) = I (a) \cap I (t))$
9		ineq2	$⊢ t = b \to a \cap t = a \cap b$
10	9	fveq2d	$⊢ t = b \to I (a \cap t) = I (a \cap b)$
11		fveq2	$⊢ t = b \to I (t) = I (b)$
12	11	ineq2d	$⊢ t = b \to I (a) \cap I (t) = I (a) \cap I (b)$
13	10 12	eqeq12d	$⊢ t = b \to (I (a \cap t) = I (a) \cap I (t) \leftrightarrow I (a \cap b) = I (a) \cap I (b))$
14	8 13	cbvral2vw	$⊢ \forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cap t) = I (s) \cap I (t) \leftrightarrow \forall a \in 𝒫 B \forall b \in 𝒫 B I (a \cap b) = I (a) \cap I (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	15	adantr	$⊢ (φ \land a \subseteq B) \to B \in V$
21		difssd	$⊢ (φ \land a \subseteq B) \to B ∖ a \subseteq B$
22	20 21	sselpwd	$⊢ (φ \land a \subseteq B) \to B ∖ a \in 𝒫 B$
23		difeq2	$⊢ s = B ∖ a \to B ∖ s = B ∖ (B ∖ a)$
24	23	eqeq2d	$⊢ s = B ∖ a \to (a = B ∖ s \leftrightarrow a = B ∖ (B ∖ a))$
25		eqcom	$⊢ a = B ∖ (B ∖ a) \leftrightarrow B ∖ (B ∖ a) = a$
26	24 25	bitrdi	$⊢ s = B ∖ a \to (a = B ∖ s \leftrightarrow B ∖ (B ∖ a) = a)$
27	26	adantl	$⊢ ((φ \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	$⊢ (φ \land a \subseteq B) \to B ∖ (B ∖ a) = a$
30	22 27 29	rspcedvd	$⊢ (φ \land a \subseteq B) \to \exists s \in 𝒫 B a = B ∖ s$
31	19 30	sylan2	$⊢ (φ \land a \in 𝒫 B) \to \exists s \in 𝒫 B a = B ∖ s$
32		ineq1	$⊢ a = B ∖ s \to a \cap b = (B ∖ s) \cap b$
33	32	fveq2d	$⊢ a = B ∖ s \to I (a \cap b) = I ((B ∖ s) \cap b)$
34		fveq2	$⊢ a = B ∖ s \to I (a) = I (B ∖ s)$
35	34	ineq1d	$⊢ a = B ∖ s \to I (a) \cap I (b) = I (B ∖ s) \cap I (b)$
36	33 35	eqeq12d	$⊢ a = B ∖ s \to (I (a \cap b) = I (a) \cap I (b) \leftrightarrow I ((B ∖ s) \cap b) = I (B ∖ s) \cap I (b))$
37	36	ralbidv	$⊢ a = B ∖ s \to (\forall b \in 𝒫 B I (a \cap b) = I (a) \cap I (b) \leftrightarrow \forall b \in 𝒫 B I ((B ∖ s) \cap b) = I (B ∖ s) \cap I (b))$
38	37	3ad2ant3	$⊢ (φ \land s \in 𝒫 B \land a = B ∖ s) \to (\forall b \in 𝒫 B I (a \cap b) = I (a) \cap I (b) \leftrightarrow \forall b \in 𝒫 B I ((B ∖ s) \cap b) = I (B ∖ s) \cap I (b))$
39		difssd	$⊢ φ \to B ∖ t \subseteq B$
40	15 39	sselpwd	$⊢ φ \to B ∖ t \in 𝒫 B$
41	40	ad2antrr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to B ∖ t \in 𝒫 B$
42		simpll	$⊢ ((φ \land s \in 𝒫 B) \land b \in 𝒫 B) \to φ$
43		elpwi	$⊢ b \in 𝒫 B \to b \subseteq B$
44	43	adantl	$⊢ ((φ \land s \in 𝒫 B) \land b \in 𝒫 B) \to b \subseteq B$
45		difssd	$⊢ φ \to B ∖ b \subseteq B$
46	15 45	sselpwd	$⊢ φ \to B ∖ b \in 𝒫 B$
47	46	adantr	$⊢ (φ \land b \subseteq B) \to B ∖ b \in 𝒫 B$
48		difeq2	$⊢ t = B ∖ b \to B ∖ t = B ∖ (B ∖ b)$
49	48	eqeq2d	$⊢ t = B ∖ b \to (b = B ∖ t \leftrightarrow b = B ∖ (B ∖ b))$
50		eqcom	$⊢ b = B ∖ (B ∖ b) \leftrightarrow B ∖ (B ∖ b) = b$
51	49 50	bitrdi	$⊢ t = B ∖ b \to (b = B ∖ t \leftrightarrow B ∖ (B ∖ b) = b)$
52	51	adantl	$⊢ ((φ \land b \subseteq B) \land t = B ∖ b) \to (b = B ∖ t \leftrightarrow B ∖ (B ∖ b) = b)$
53		dfss4	$⊢ b \subseteq B \leftrightarrow B ∖ (B ∖ b) = b$
54	53	bilani	$⊢ (φ \land b \subseteq B) \to B ∖ (B ∖ b) = b$
55	47 52 54	rspcedvd	$⊢ (φ \land b \subseteq B) \to \exists t \in 𝒫 B b = B ∖ t$
56	42 44 55	syl2anc	$⊢ ((φ \land s \in 𝒫 B) \land b \in 𝒫 B) \to \exists t \in 𝒫 B b = B ∖ t$
57		ineq2	$⊢ b = B ∖ t \to (B ∖ s) \cap b = (B ∖ s) \cap (B ∖ t)$
58		difundi	$⊢ B ∖ (s \cup t) = (B ∖ s) \cap (B ∖ t)$
59	57 58	eqtr4di	$⊢ b = B ∖ t \to (B ∖ s) \cap b = B ∖ (s \cup t)$
60	59	fveq2d	$⊢ b = B ∖ t \to I ((B ∖ s) \cap b) = I (B ∖ (s \cup t))$
61		fveq2	$⊢ b = B ∖ t \to I (b) = I (B ∖ t)$
62	61	ineq2d	$⊢ b = B ∖ t \to I (B ∖ s) \cap I (b) = I (B ∖ s) \cap I (B ∖ t)$
63	60 62	eqeq12d	$⊢ b = B ∖ t \to (I ((B ∖ s) \cap b) = I (B ∖ s) \cap I (b) \leftrightarrow I (B ∖ (s \cup t)) = I (B ∖ s) \cap I (B ∖ t))$
64	63	3ad2ant3	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B \land b = B ∖ t) \to (I ((B ∖ s) \cap b) = I (B ∖ s) \cap I (b) \leftrightarrow I (B ∖ (s \cup t)) = I (B ∖ s) \cap I (B ∖ t))$
65		simp1l	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B \land b = B ∖ t) \to φ$
66	65 15	jccir	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B \land b = B ∖ t) \to (φ \land B \in V)$
67		simp1r	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B \land b = B ∖ t) \to s \in 𝒫 B$
68		simp2	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B \land b = B ∖ t) \to t \in 𝒫 B$
69	1 2 3	ntrclsiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
70		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
71	69 70	syl	$⊢ φ \to I : 𝒫 B ⟶ 𝒫 B$
72	71	anim1i	$⊢ (φ \land B \in V) \to (I : 𝒫 B ⟶ 𝒫 B \land B \in V)$
73	72	adantr	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to (I : 𝒫 B ⟶ 𝒫 B \land B \in V)$
74		simpl	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to I : 𝒫 B ⟶ 𝒫 B$
75		simpr	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to B \in V$
76		difssd	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to B ∖ (s \cup t) \subseteq B$
77	75 76	sselpwd	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to B ∖ (s \cup t) \in 𝒫 B$
78	74 77	ffvelcdmd	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to I (B ∖ (s \cup t)) \in 𝒫 B$
79	78	elpwid	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to I (B ∖ (s \cup t)) \subseteq B$
80		difssd	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to B ∖ s \subseteq B$
81	75 80	sselpwd	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to B ∖ s \in 𝒫 B$
82	74 81	ffvelcdmd	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to I (B ∖ s) \in 𝒫 B$
83	82	elpwid	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to I (B ∖ s) \subseteq B$
84		ssinss1	$⊢ I (B ∖ s) \subseteq B \to I (B ∖ s) \cap I (B ∖ t) \subseteq B$
85	83 84	syl	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to I (B ∖ s) \cap I (B ∖ t) \subseteq B$
86	79 85	jca	$⊢ (I : 𝒫 B ⟶ 𝒫 B \land B \in V) \to (I (B ∖ (s \cup t)) \subseteq B \land I (B ∖ s) \cap I (B ∖ t) \subseteq B)$
87		rcompleq	$⊢ (I (B ∖ (s \cup t)) \subseteq B \land I (B ∖ s) \cap I (B ∖ t) \subseteq B) \to (I (B ∖ (s \cup t)) = I (B ∖ s) \cap I (B ∖ t) \leftrightarrow B ∖ I (B ∖ (s \cup t)) = B ∖ (I (B ∖ s) \cap I (B ∖ t)))$
88	73 86 87	3syl	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to (I (B ∖ (s \cup t)) = I (B ∖ s) \cap I (B ∖ t) \leftrightarrow B ∖ I (B ∖ (s \cup t)) = B ∖ (I (B ∖ s) \cap I (B ∖ t)))$
89		simplr	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to B \in V$
90	69	ad2antrr	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to I \in ({𝒫 B}^{𝒫 B})$
91		eqid	$⊢ D (I) = D (I)$
92		simprl	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \in 𝒫 B$
93	92	elpwid	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \subseteq B$
94		simprr	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to t \in 𝒫 B$
95	94	elpwid	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to t \subseteq B$
96	93 95	unssd	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \cup t \subseteq B$
97	89 96	sselpwd	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to s \cup t \in 𝒫 B$
98		eqid	$⊢ D (I) (s \cup t) = D (I) (s \cup t)$
99	1 2 89 90 91 97 98	dssmapfv3d	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (s \cup t) = B ∖ I (B ∖ (s \cup t))$
100		simpl	$⊢ (s \in 𝒫 B \land t \in 𝒫 B) \to s \in 𝒫 B$
101		simplr	$⊢ ((φ \land B \in V) \land s \in 𝒫 B) \to B \in V$
102	69	ad2antrr	$⊢ ((φ \land B \in V) \land s \in 𝒫 B) \to I \in ({𝒫 B}^{𝒫 B})$
103		simpr	$⊢ ((φ \land B \in V) \land s \in 𝒫 B) \to s \in 𝒫 B$
104		eqid	$⊢ D (I) (s) = D (I) (s)$
105	1 2 101 102 91 103 104	dssmapfv3d	$⊢ ((φ \land B \in V) \land s \in 𝒫 B) \to D (I) (s) = B ∖ I (B ∖ s)$
106	100 105	sylan2	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (s) = B ∖ I (B ∖ s)$
107		simpr	$⊢ (s \in 𝒫 B \land t \in 𝒫 B) \to t \in 𝒫 B$
108		simplr	$⊢ ((φ \land B \in V) \land t \in 𝒫 B) \to B \in V$
109	69	ad2antrr	$⊢ ((φ \land B \in V) \land t \in 𝒫 B) \to I \in ({𝒫 B}^{𝒫 B})$
110		simpr	$⊢ ((φ \land B \in V) \land t \in 𝒫 B) \to t \in 𝒫 B$
111		eqid	$⊢ D (I) (t) = D (I) (t)$
112	1 2 108 109 91 110 111	dssmapfv3d	$⊢ ((φ \land B \in V) \land t \in 𝒫 B) \to D (I) (t) = B ∖ I (B ∖ t)$
113	107 112	sylan2	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (t) = B ∖ I (B ∖ t)$
114	106 113	uneq12d	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (s) \cup D (I) (t) = (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t))$
115		difindi	$⊢ B ∖ (I (B ∖ s) \cap I (B ∖ t)) = (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t))$
116	114 115	eqtr4di	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to D (I) (s) \cup D (I) (t) = B ∖ (I (B ∖ s) \cap I (B ∖ t))$
117	99 116	eqeq12d	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to (D (I) (s \cup t) = D (I) (s) \cup D (I) (t) \leftrightarrow B ∖ I (B ∖ (s \cup t)) = B ∖ (I (B ∖ s) \cap I (B ∖ t)))$
118		simpll	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to φ$
119	1 2 3	ntrclsfv1	$⊢ φ \to D (I) = K$
120		fveq1	$⊢ D (I) = K \to D (I) (s \cup t) = K (s \cup t)$
121		fveq1	$⊢ D (I) = K \to D (I) (s) = K (s)$
122		fveq1	$⊢ D (I) = K \to D (I) (t) = K (t)$
123	121 122	uneq12d	$⊢ D (I) = K \to D (I) (s) \cup D (I) (t) = K (s) \cup K (t)$
124	120 123	eqeq12d	$⊢ D (I) = K \to (D (I) (s \cup t) = D (I) (s) \cup D (I) (t) \leftrightarrow K (s \cup t) = K (s) \cup K (t))$
125	118 119 124	3syl	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to (D (I) (s \cup t) = D (I) (s) \cup D (I) (t) \leftrightarrow K (s \cup t) = K (s) \cup K (t))$
126	88 117 125	3bitr2d	$⊢ ((φ \land B \in V) \land (s \in 𝒫 B \land t \in 𝒫 B)) \to (I (B ∖ (s \cup t)) = I (B ∖ s) \cap I (B ∖ t) \leftrightarrow K (s \cup t) = K (s) \cup K (t))$
127	66 67 68 126	syl12anc	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B \land b = B ∖ t) \to (I (B ∖ (s \cup t)) = I (B ∖ s) \cap I (B ∖ t) \leftrightarrow K (s \cup t) = K (s) \cup K (t))$
128	64 127	bitrd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B \land b = B ∖ t) \to (I ((B ∖ s) \cap b) = I (B ∖ s) \cap I (b) \leftrightarrow K (s \cup t) = K (s) \cup K (t))$
129	41 56 128	ralxfrd2	$⊢ (φ \land s \in 𝒫 B) \to (\forall b \in 𝒫 B I ((B ∖ s) \cap b) = I (B ∖ s) \cap I (b) \leftrightarrow \forall t \in 𝒫 B K (s \cup t) = K (s) \cup K (t))$
130	129	3adant3	$⊢ (φ \land s \in 𝒫 B \land a = B ∖ s) \to (\forall b \in 𝒫 B I ((B ∖ s) \cap b) = I (B ∖ s) \cap I (b) \leftrightarrow \forall t \in 𝒫 B K (s \cup t) = K (s) \cup K (t))$
131	38 130	bitrd	$⊢ (φ \land s \in 𝒫 B \land a = B ∖ s) \to (\forall b \in 𝒫 B I (a \cap b) = I (a) \cap I (b) \leftrightarrow \forall t \in 𝒫 B K (s \cup t) = K (s) \cup K (t))$
132	18 31 131	ralxfrd2	$⊢ φ \to (\forall a \in 𝒫 B \forall b \in 𝒫 B I (a \cap b) = I (a) \cap I (b) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B K (s \cup t) = K (s) \cup K (t))$
133	14 132	bitrid	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cap t) = I (s) \cap I (t) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B K (s \cup t) = K (s) \cup K (t))$

Metamath Proof Explorer

Theorem ntrclsk13

Proof