sepnsepo

Description: Open neighborhood and neighborhood is equivalent regarding disjointness for both sides. Namely, separatedness by open neighborhoods is equivalent to separatedness by neighborhoods. (Contributed by Zhi Wang, 1-Sep-2024)

		Ref	Expression
	Hypothesis	sepnsepolem2.1	$⊢ φ \to J \in Top$
	Assertion	sepnsepo	$⊢ φ \to (\exists x \in nei (J) (C) \exists y \in nei (J) (D) x \cap y = \emptyset \leftrightarrow \exists x \in J \exists y \in J (C \subseteq x \land D \subseteq y \land x \cap y = \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		sepnsepolem2.1	$⊢ φ \to J \in Top$
2		id	$⊢ J \in Top \to J \in Top$
3	2	sepnsepolem2	$⊢ J \in Top \to (\exists y \in nei (J) (D) x \cap y = \emptyset \leftrightarrow \exists y \in J (D \subseteq y \land x \cap y = \emptyset))$
4	3	anbi2d	$⊢ J \in Top \to ((C \subseteq x \land \exists y \in nei (J) (D) x \cap y = \emptyset) \leftrightarrow (C \subseteq x \land \exists y \in J (D \subseteq y \land x \cap y = \emptyset)))$
5	4	rexbidv	$⊢ J \in Top \to (\exists x \in J (C \subseteq x \land \exists y \in nei (J) (D) x \cap y = \emptyset) \leftrightarrow \exists x \in J (C \subseteq x \land \exists y \in J (D \subseteq y \land x \cap y = \emptyset)))$
6		ssrin	$⊢ z \subseteq x \to z \cap y \subseteq x \cap y$
7		sseq0	$⊢ (z \cap y \subseteq x \cap y \land x \cap y = \emptyset) \to z \cap y = \emptyset$
8	7	ex	$⊢ z \cap y \subseteq x \cap y \to (x \cap y = \emptyset \to z \cap y = \emptyset)$
9	6 8	syl	$⊢ z \subseteq x \to (x \cap y = \emptyset \to z \cap y = \emptyset)$
10	9	adantl	$⊢ (J \in Top \land z \subseteq x) \to (x \cap y = \emptyset \to z \cap y = \emptyset)$
11	10	reximdv	$⊢ (J \in Top \land z \subseteq x) \to (\exists y \in nei (J) (D) x \cap y = \emptyset \to \exists y \in nei (J) (D) z \cap y = \emptyset)$
12		simpr	$⊢ (J \in Top \land x = z) \to x = z$
13	12	ineq1d	$⊢ (J \in Top \land x = z) \to x \cap y = z \cap y$
14	13	eqeq1d	$⊢ (J \in Top \land x = z) \to (x \cap y = \emptyset \leftrightarrow z \cap y = \emptyset)$
15	14	rexbidv	$⊢ (J \in Top \land x = z) \to (\exists y \in nei (J) (D) x \cap y = \emptyset \leftrightarrow \exists y \in nei (J) (D) z \cap y = \emptyset)$
16	2 11 15	opnneibid	$⊢ J \in Top \to (\exists x \in nei (J) (C) \exists y \in nei (J) (D) x \cap y = \emptyset \leftrightarrow \exists x \in J (C \subseteq x \land \exists y \in nei (J) (D) x \cap y = \emptyset))$
17		sepnsepolem1	$⊢ \exists x \in J \exists y \in J (C \subseteq x \land D \subseteq y \land x \cap y = \emptyset) \leftrightarrow \exists x \in J (C \subseteq x \land \exists y \in J (D \subseteq y \land x \cap y = \emptyset))$
18	17	a1i	$⊢ J \in Top \to (\exists x \in J \exists y \in J (C \subseteq x \land D \subseteq y \land x \cap y = \emptyset) \leftrightarrow \exists x \in J (C \subseteq x \land \exists y \in J (D \subseteq y \land x \cap y = \emptyset)))$
19	5 16 18	3bitr4d	$⊢ J \in Top \to (\exists x \in nei (J) (C) \exists y \in nei (J) (D) x \cap y = \emptyset \leftrightarrow \exists x \in J \exists y \in J (C \subseteq x \land D \subseteq y \land x \cap y = \emptyset))$
20	1 19	syl	$⊢ φ \to (\exists x \in nei (J) (C) \exists y \in nei (J) (D) x \cap y = \emptyset \leftrightarrow \exists x \in J \exists y \in J (C \subseteq x \land D \subseteq y \land x \cap y = \emptyset))$

Metamath Proof Explorer

Theorem sepnsepo

Proof