ntrk0kbimka

Description: If the interiors of disjoint sets are disjoint and the interior of the base set is the base set, then the interior of the empty set is the empty set. Obsolete version of ntrkbimka . (Contributed by RP, 12-Jun-2021)

		Ref	Expression
	Assertion	ntrk0kbimka	$⊢ (B \in V \land I \in ({𝒫 B}^{𝒫 B})) \to ((I (B) = B \land \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset)) \to I (\emptyset) = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		pwidg	$⊢ B \in V \to B \in 𝒫 B$
2	1	ad2antrr	$⊢ ((B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (I (B) = B \land \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset))) \to B \in 𝒫 B$
3		0elpw	$⊢ \emptyset \in 𝒫 B$
4	3	a1i	$⊢ ((B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (I (B) = B \land \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset))) \to \emptyset \in 𝒫 B$
5		simprr	$⊢ ((B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (I (B) = B \land \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset))) \to \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset)$
6		ineq1	$⊢ s = B \to s \cap t = B \cap t$
7	6	eqeq1d	$⊢ s = B \to (s \cap t = \emptyset \leftrightarrow B \cap t = \emptyset)$
8		fveq2	$⊢ s = B \to I (s) = I (B)$
9	8	ineq1d	$⊢ s = B \to I (s) \cap I (t) = I (B) \cap I (t)$
10	9	eqeq1d	$⊢ s = B \to (I (s) \cap I (t) = \emptyset \leftrightarrow I (B) \cap I (t) = \emptyset)$
11	7 10	imbi12d	$⊢ s = B \to ((s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset) \leftrightarrow (B \cap t = \emptyset \to I (B) \cap I (t) = \emptyset))$
12		ineq2	$⊢ t = \emptyset \to B \cap t = B \cap \emptyset$
13	12	eqeq1d	$⊢ t = \emptyset \to (B \cap t = \emptyset \leftrightarrow B \cap \emptyset = \emptyset)$
14		fveq2	$⊢ t = \emptyset \to I (t) = I (\emptyset)$
15	14	ineq2d	$⊢ t = \emptyset \to I (B) \cap I (t) = I (B) \cap I (\emptyset)$
16	15	eqeq1d	$⊢ t = \emptyset \to (I (B) \cap I (t) = \emptyset \leftrightarrow I (B) \cap I (\emptyset) = \emptyset)$
17	13 16	imbi12d	$⊢ t = \emptyset \to ((B \cap t = \emptyset \to I (B) \cap I (t) = \emptyset) \leftrightarrow (B \cap \emptyset = \emptyset \to I (B) \cap I (\emptyset) = \emptyset))$
18		in0	$⊢ B \cap \emptyset = \emptyset$
19		pm5.5	$⊢ B \cap \emptyset = \emptyset \to ((B \cap \emptyset = \emptyset \to I (B) \cap I (\emptyset) = \emptyset) \leftrightarrow I (B) \cap I (\emptyset) = \emptyset)$
20	18 19	mp1i	$⊢ t = \emptyset \to ((B \cap \emptyset = \emptyset \to I (B) \cap I (\emptyset) = \emptyset) \leftrightarrow I (B) \cap I (\emptyset) = \emptyset)$
21	17 20	bitrd	$⊢ t = \emptyset \to ((B \cap t = \emptyset \to I (B) \cap I (t) = \emptyset) \leftrightarrow I (B) \cap I (\emptyset) = \emptyset)$
22	11 21	rspc2va	$⊢ ((B \in 𝒫 B \land \emptyset \in 𝒫 B) \land \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset)) \to I (B) \cap I (\emptyset) = \emptyset$
23	2 4 5 22	syl21anc	$⊢ ((B \in V \land I \in ({𝒫 B}^{𝒫 B})) \land (I (B) = B \land \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset))) \to I (B) \cap I (\emptyset) = \emptyset$
24	23	ex	$⊢ (B \in V \land I \in ({𝒫 B}^{𝒫 B})) \to ((I (B) = B \land \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset)) \to I (B) \cap I (\emptyset) = \emptyset)$
25		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
26	25	adantl	$⊢ (B \in V \land I \in ({𝒫 B}^{𝒫 B})) \to I : 𝒫 B ⟶ 𝒫 B$
27	3	a1i	$⊢ (B \in V \land I \in ({𝒫 B}^{𝒫 B})) \to \emptyset \in 𝒫 B$
28	26 27	ffvelcdmd	$⊢ (B \in V \land I \in ({𝒫 B}^{𝒫 B})) \to I (\emptyset) \in 𝒫 B$
29	28	elpwid	$⊢ (B \in V \land I \in ({𝒫 B}^{𝒫 B})) \to I (\emptyset) \subseteq B$
30		simpl	$⊢ (I (B) = B \land \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset)) \to I (B) = B$
31		ineq1	$⊢ I (B) = B \to I (B) \cap I (\emptyset) = B \cap I (\emptyset)$
32		incom	$⊢ B \cap I (\emptyset) = I (\emptyset) \cap B$
33	31 32	eqtrdi	$⊢ I (B) = B \to I (B) \cap I (\emptyset) = I (\emptyset) \cap B$
34	33	eqeq1d	$⊢ I (B) = B \to (I (B) \cap I (\emptyset) = \emptyset \leftrightarrow I (\emptyset) \cap B = \emptyset)$
35	34	biimpd	$⊢ I (B) = B \to (I (B) \cap I (\emptyset) = \emptyset \to I (\emptyset) \cap B = \emptyset)$
36		reldisj	$⊢ I (\emptyset) \subseteq B \to (I (\emptyset) \cap B = \emptyset \leftrightarrow I (\emptyset) \subseteq B ∖ B)$
37	36	biimpd	$⊢ I (\emptyset) \subseteq B \to (I (\emptyset) \cap B = \emptyset \to I (\emptyset) \subseteq B ∖ B)$
38		difid	$⊢ B ∖ B = \emptyset$
39	38	sseq2i	$⊢ I (\emptyset) \subseteq B ∖ B \leftrightarrow I (\emptyset) \subseteq \emptyset$
40		ss0	$⊢ I (\emptyset) \subseteq \emptyset \to I (\emptyset) = \emptyset$
41	39 40	sylbi	$⊢ I (\emptyset) \subseteq B ∖ B \to I (\emptyset) = \emptyset$
42	37 41	syl6com	$⊢ I (\emptyset) \cap B = \emptyset \to (I (\emptyset) \subseteq B \to I (\emptyset) = \emptyset)$
43	35 42	syl6com	$⊢ I (B) \cap I (\emptyset) = \emptyset \to (I (B) = B \to (I (\emptyset) \subseteq B \to I (\emptyset) = \emptyset))$
44	43	com13	$⊢ I (\emptyset) \subseteq B \to (I (B) = B \to (I (B) \cap I (\emptyset) = \emptyset \to I (\emptyset) = \emptyset))$
45	29 30 44	syl2im	$⊢ (B \in V \land I \in ({𝒫 B}^{𝒫 B})) \to ((I (B) = B \land \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset)) \to (I (B) \cap I (\emptyset) = \emptyset \to I (\emptyset) = \emptyset))$
46	24 45	mpdd	$⊢ (B \in V \land I \in ({𝒫 B}^{𝒫 B})) \to ((I (B) = B \land \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset)) \to I (\emptyset) = \emptyset)$

Metamath Proof Explorer

Theorem ntrk0kbimka

Proof