ntrclskb

Description: The interiors of disjoint sets are disjoint if and only if the closures of sets that span the base set also span the base set. (Contributed by RP, 10-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	ntrclskb	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cup t = B \to K (s) \cup K (t) = B))$

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	eqeq1d	$⊢ s = a \to (s \cap t = \emptyset \leftrightarrow a \cap t = \emptyset)$
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	7	eqeq1d	$⊢ s = a \to (I (s) \cap I (t) = \emptyset \leftrightarrow I (a) \cap I (t) = \emptyset)$
9	5 8	imbi12d	$⊢ s = a \to ((s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset) \leftrightarrow (a \cap t = \emptyset \to I (a) \cap I (t) = \emptyset))$
10		ineq2	$⊢ t = b \to a \cap t = a \cap b$
11	10	eqeq1d	$⊢ t = b \to (a \cap t = \emptyset \leftrightarrow a \cap b = \emptyset)$
12		fveq2	$⊢ t = b \to I (t) = I (b)$
13	12	ineq2d	$⊢ t = b \to I (a) \cap I (t) = I (a) \cap I (b)$
14	13	eqeq1d	$⊢ t = b \to (I (a) \cap I (t) = \emptyset \leftrightarrow I (a) \cap I (b) = \emptyset)$
15	11 14	imbi12d	$⊢ t = b \to ((a \cap t = \emptyset \to I (a) \cap I (t) = \emptyset) \leftrightarrow (a \cap b = \emptyset \to I (a) \cap I (b) = \emptyset))$
16	9 15	cbvral2vw	$⊢ \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset) \leftrightarrow \forall a \in 𝒫 B \forall b \in 𝒫 B (a \cap b = \emptyset \to I (a) \cap I (b) = \emptyset)$
17	2 3	ntrclsrcomplex	$⊢ φ \to B ∖ s \in 𝒫 B$
18	17	adantr	$⊢ (φ \land s \in 𝒫 B) \to B ∖ s \in 𝒫 B$
19	2 3	ntrclsrcomplex	$⊢ φ \to B ∖ a \in 𝒫 B$
20	19	adantr	$⊢ (φ \land a \in 𝒫 B) \to B ∖ a \in 𝒫 B$
21		difeq2	$⊢ s = B ∖ a \to B ∖ s = B ∖ (B ∖ a)$
22	21	eqeq2d	$⊢ s = B ∖ a \to (a = B ∖ s \leftrightarrow a = B ∖ (B ∖ a))$
23	22	adantl	$⊢ ((φ \land a \in 𝒫 B) \land s = B ∖ a) \to (a = B ∖ s \leftrightarrow a = B ∖ (B ∖ a))$
24		elpwi	$⊢ a \in 𝒫 B \to a \subseteq B$
25		dfss4	$⊢ a \subseteq B \leftrightarrow B ∖ (B ∖ a) = a$
26	24 25	sylib	$⊢ a \in 𝒫 B \to B ∖ (B ∖ a) = a$
27	26	eqcomd	$⊢ a \in 𝒫 B \to a = B ∖ (B ∖ a)$
28	27	adantl	$⊢ (φ \land a \in 𝒫 B) \to a = B ∖ (B ∖ a)$
29	20 23 28	rspcedvd	$⊢ (φ \land a \in 𝒫 B) \to \exists s \in 𝒫 B a = B ∖ s$
30		simpl1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to φ$
31	2 3	ntrclsrcomplex	$⊢ φ \to B ∖ t \in 𝒫 B$
32	30 31	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to B ∖ t \in 𝒫 B$
33	2 3	ntrclsrcomplex	$⊢ φ \to B ∖ b \in 𝒫 B$
34	33	adantr	$⊢ (φ \land b \in 𝒫 B) \to B ∖ b \in 𝒫 B$
35		difeq2	$⊢ t = B ∖ b \to B ∖ t = B ∖ (B ∖ b)$
36	35	eqeq2d	$⊢ t = B ∖ b \to (b = B ∖ t \leftrightarrow b = B ∖ (B ∖ b))$
37	36	adantl	$⊢ ((φ \land b \in 𝒫 B) \land t = B ∖ b) \to (b = B ∖ t \leftrightarrow b = B ∖ (B ∖ b))$
38		elpwi	$⊢ b \in 𝒫 B \to b \subseteq B$
39		dfss4	$⊢ b \subseteq B \leftrightarrow B ∖ (B ∖ b) = b$
40	38 39	sylib	$⊢ b \in 𝒫 B \to B ∖ (B ∖ b) = b$
41	40	eqcomd	$⊢ b \in 𝒫 B \to b = B ∖ (B ∖ b)$
42	41	adantl	$⊢ (φ \land b \in 𝒫 B) \to b = B ∖ (B ∖ b)$
43	34 37 42	rspcedvd	$⊢ (φ \land b \in 𝒫 B) \to \exists t \in 𝒫 B b = B ∖ t$
44	43	3ad2antl1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land b \in 𝒫 B) \to \exists t \in 𝒫 B b = B ∖ t$
45		simp13	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to a = B ∖ s$
46		ineq1	$⊢ a = B ∖ s \to a \cap b = (B ∖ s) \cap b$
47	46	eqeq1d	$⊢ a = B ∖ s \to (a \cap b = \emptyset \leftrightarrow (B ∖ s) \cap b = \emptyset)$
48		fveq2	$⊢ a = B ∖ s \to I (a) = I (B ∖ s)$
49	48	ineq1d	$⊢ a = B ∖ s \to I (a) \cap I (b) = I (B ∖ s) \cap I (b)$
50	49	eqeq1d	$⊢ a = B ∖ s \to (I (a) \cap I (b) = \emptyset \leftrightarrow I (B ∖ s) \cap I (b) = \emptyset)$
51	47 50	imbi12d	$⊢ a = B ∖ s \to ((a \cap b = \emptyset \to I (a) \cap I (b) = \emptyset) \leftrightarrow ((B ∖ s) \cap b = \emptyset \to I (B ∖ s) \cap I (b) = \emptyset))$
52	45 51	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to ((a \cap b = \emptyset \to I (a) \cap I (b) = \emptyset) \leftrightarrow ((B ∖ s) \cap b = \emptyset \to I (B ∖ s) \cap I (b) = \emptyset))$
53		simp3	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to b = B ∖ t$
54		ineq2	$⊢ b = B ∖ t \to (B ∖ s) \cap b = (B ∖ s) \cap (B ∖ t)$
55	54	eqeq1d	$⊢ b = B ∖ t \to ((B ∖ s) \cap b = \emptyset \leftrightarrow (B ∖ s) \cap (B ∖ t) = \emptyset)$
56		fveq2	$⊢ b = B ∖ t \to I (b) = I (B ∖ t)$
57	56	ineq2d	$⊢ b = B ∖ t \to I (B ∖ s) \cap I (b) = I (B ∖ s) \cap I (B ∖ t)$
58	57	eqeq1d	$⊢ b = B ∖ t \to (I (B ∖ s) \cap I (b) = \emptyset \leftrightarrow I (B ∖ s) \cap I (B ∖ t) = \emptyset)$
59	55 58	imbi12d	$⊢ b = B ∖ t \to (((B ∖ s) \cap b = \emptyset \to I (B ∖ s) \cap I (b) = \emptyset) \leftrightarrow ((B ∖ s) \cap (B ∖ t) = \emptyset \to I (B ∖ s) \cap I (B ∖ t) = \emptyset))$
60	53 59	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (((B ∖ s) \cap b = \emptyset \to I (B ∖ s) \cap I (b) = \emptyset) \leftrightarrow ((B ∖ s) \cap (B ∖ t) = \emptyset \to I (B ∖ s) \cap I (B ∖ t) = \emptyset))$
61		simp11	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to φ$
62		simp12	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to s \in 𝒫 B$
63		simp2	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to t \in 𝒫 B$
64		simp2	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to s \in 𝒫 B$
65	64	elpwid	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to s \subseteq B$
66		simp3	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to t \in 𝒫 B$
67	66	elpwid	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to t \subseteq B$
68	65 67	unssd	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to s \cup t \subseteq B$
69		ssid	$⊢ B \subseteq B$
70		rcompleq	$⊢ (s \cup t \subseteq B \land B \subseteq B) \to (s \cup t = B \leftrightarrow B ∖ (s \cup t) = B ∖ B)$
71	68 69 70	sylancl	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to (s \cup t = B \leftrightarrow B ∖ (s \cup t) = B ∖ B)$
72		difundi	$⊢ B ∖ (s \cup t) = (B ∖ s) \cap (B ∖ t)$
73		difid	$⊢ B ∖ B = \emptyset$
74	72 73	eqeq12i	$⊢ B ∖ (s \cup t) = B ∖ B \leftrightarrow (B ∖ s) \cap (B ∖ t) = \emptyset$
75	71 74	bitr2di	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to ((B ∖ s) \cap (B ∖ t) = \emptyset \leftrightarrow s \cup t = B)$
76	1 2 3	ntrclsiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
77	76	3ad2ant1	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to I \in ({𝒫 B}^{𝒫 B})$
78		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
79	77 78	syl	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to I : 𝒫 B ⟶ 𝒫 B$
80	2 3	ntrclsbex	$⊢ φ \to B \in V$
81	80	3ad2ant1	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to B \in V$
82		difssd	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to B ∖ s \subseteq B$
83	81 82	sselpwd	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to B ∖ s \in 𝒫 B$
84	79 83	ffvelcdmd	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to I (B ∖ s) \in 𝒫 B$
85	84	elpwid	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \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	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to I (B ∖ s) \cap I (B ∖ t) \subseteq B$
88		0ss	$⊢ \emptyset \subseteq B$
89		rcompleq	$⊢ (I (B ∖ s) \cap I (B ∖ t) \subseteq B \land \emptyset \subseteq B) \to (I (B ∖ s) \cap I (B ∖ t) = \emptyset \leftrightarrow B ∖ (I (B ∖ s) \cap I (B ∖ t)) = B ∖ \emptyset)$
90	87 88 89	sylancl	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to (I (B ∖ s) \cap I (B ∖ t) = \emptyset \leftrightarrow B ∖ (I (B ∖ s) \cap I (B ∖ t)) = B ∖ \emptyset)$
91		difindi	$⊢ B ∖ (I (B ∖ s) \cap I (B ∖ t)) = (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t))$
92		dif0	$⊢ B ∖ \emptyset = B$
93	91 92	eqeq12i	$⊢ B ∖ (I (B ∖ s) \cap I (B ∖ t)) = B ∖ \emptyset \leftrightarrow (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t)) = B$
94	90 93	bitrdi	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to (I (B ∖ s) \cap I (B ∖ t) = \emptyset \leftrightarrow (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t)) = B)$
95	75 94	imbi12d	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to (((B ∖ s) \cap (B ∖ t) = \emptyset \to I (B ∖ s) \cap I (B ∖ t) = \emptyset) \leftrightarrow (s \cup t = B \to (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t)) = B))$
96		eqid	$⊢ D (I) = D (I)$
97		eqid	$⊢ D (I) (s) = D (I) (s)$
98	1 2 81 77 96 64 97	dssmapfv3d	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to D (I) (s) = B ∖ I (B ∖ s)$
99		eqid	$⊢ D (I) (t) = D (I) (t)$
100	1 2 81 77 96 66 99	dssmapfv3d	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to D (I) (t) = B ∖ I (B ∖ t)$
101	98 100	uneq12d	$⊢ (φ \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))$
102	1 2 3	ntrclsfv1	$⊢ φ \to D (I) = K$
103	102	3ad2ant1	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to D (I) = K$
104		fveq1	$⊢ D (I) = K \to D (I) (s) = K (s)$
105		fveq1	$⊢ D (I) = K \to D (I) (t) = K (t)$
106	104 105	uneq12d	$⊢ D (I) = K \to D (I) (s) \cup D (I) (t) = K (s) \cup K (t)$
107	103 106	syl	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to D (I) (s) \cup D (I) (t) = K (s) \cup K (t)$
108	101 107	eqtr3d	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t)) = K (s) \cup K (t)$
109	108	eqeq1d	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to ((B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t)) = B \leftrightarrow K (s) \cup K (t) = B)$
110	109	imbi2d	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to ((s \cup t = B \to (B ∖ I (B ∖ s)) \cup (B ∖ I (B ∖ t)) = B) \leftrightarrow (s \cup t = B \to K (s) \cup K (t) = B))$
111	95 110	bitrd	$⊢ (φ \land s \in 𝒫 B \land t \in 𝒫 B) \to (((B ∖ s) \cap (B ∖ t) = \emptyset \to I (B ∖ s) \cap I (B ∖ t) = \emptyset) \leftrightarrow (s \cup t = B \to K (s) \cup K (t) = B))$
112	61 62 63 111	syl3anc	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (((B ∖ s) \cap (B ∖ t) = \emptyset \to I (B ∖ s) \cap I (B ∖ t) = \emptyset) \leftrightarrow (s \cup t = B \to K (s) \cup K (t) = B))$
113	52 60 112	3bitrd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to ((a \cap b = \emptyset \to I (a) \cap I (b) = \emptyset) \leftrightarrow (s \cup t = B \to K (s) \cup K (t) = B))$
114	32 44 113	ralxfrd2	$⊢ (φ \land s \in 𝒫 B \land a = B ∖ s) \to (\forall b \in 𝒫 B (a \cap b = \emptyset \to I (a) \cap I (b) = \emptyset) \leftrightarrow \forall t \in 𝒫 B (s \cup t = B \to K (s) \cup K (t) = B))$
115	18 29 114	ralxfrd2	$⊢ φ \to (\forall a \in 𝒫 B \forall b \in 𝒫 B (a \cap b = \emptyset \to I (a) \cap I (b) = \emptyset) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cup t = B \to K (s) \cup K (t) = B))$
116	16 115	bitrid	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cup t = B \to K (s) \cup K (t) = B))$

Metamath Proof Explorer

Theorem ntrclskb

Proof