Metamath Proof Explorer

Theorem sepnsepolem2

Description: Open neighborhood and neighborhood is equivalent regarding disjointness. Lemma for sepnsepo . Proof could be shortened by 1 step using ssdisjdr . (Contributed by Zhi Wang, 1-Sep-2024)

		Ref	Expression
	Hypothesis	sepnsepolem2.1	$⊢ φ \to J \in Top$
	Assertion	sepnsepolem2	$⊢ φ \to (\exists y \in nei (J) (D) x \cap y = \emptyset \leftrightarrow \exists y \in J (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		sslin	$⊢ z \subseteq y \to x \cap z \subseteq x \cap y$
4		sseq0	$⊢ (x \cap z \subseteq x \cap y \land x \cap y = \emptyset) \to x \cap z = \emptyset$
5	4	ex	$⊢ x \cap z \subseteq x \cap y \to (x \cap y = \emptyset \to x \cap z = \emptyset)$
6	3 5	syl	$⊢ z \subseteq y \to (x \cap y = \emptyset \to x \cap z = \emptyset)$
7	6	adantl	$⊢ (J \in Top \land z \subseteq y) \to (x \cap y = \emptyset \to x \cap z = \emptyset)$
8		ineq2	$⊢ y = z \to x \cap y = x \cap z$
9	8	eqeq1d	$⊢ y = z \to (x \cap y = \emptyset \leftrightarrow x \cap z = \emptyset)$
10	9	adantl	$⊢ (J \in Top \land y = z) \to (x \cap y = \emptyset \leftrightarrow x \cap z = \emptyset)$
11	2 7 10	opnneieqv	$⊢ 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))$
12	1 11	syl	$⊢ φ \to (\exists y \in nei (J) (D) x \cap y = \emptyset \leftrightarrow \exists y \in J (D \subseteq y \land x \cap y = \emptyset))$