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