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	⊢ ( 𝜑 → 𝐽 ∈ Top )
Assertion	sepnsepolem2	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ 𝐽 ( 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		sepnsepolem2.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		id	⊢ ( 𝐽 ∈ Top → 𝐽 ∈ Top )
3		sslin	⊢ ( 𝑧 ⊆ 𝑦 → ( 𝑥 ∩ 𝑧 ) ⊆ ( 𝑥 ∩ 𝑦 ) )
4		sseq0	⊢ ( ( ( 𝑥 ∩ 𝑧 ) ⊆ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∩ 𝑧 ) = ∅ )
5	4	ex	⊢ ( ( 𝑥 ∩ 𝑧 ) ⊆ ( 𝑥 ∩ 𝑦 ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑥 ∩ 𝑧 ) = ∅ ) )
6	3 5	syl	⊢ ( 𝑧 ⊆ 𝑦 → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑥 ∩ 𝑧 ) = ∅ ) )
7	6	adantl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑧 ⊆ 𝑦 ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑥 ∩ 𝑧 ) = ∅ ) )
8		ineq2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 ∩ 𝑦 ) = ( 𝑥 ∩ 𝑧 ) )
9	8	eqeq1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ( 𝑥 ∩ 𝑧 ) = ∅ ) )
10	9	adantl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 = 𝑧 ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ( 𝑥 ∩ 𝑧 ) = ∅ ) )
11	2 7 10	opnneieqv	⊢ ( 𝐽 ∈ Top → ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ 𝐽 ( 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )
12	1 11	syl	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ 𝐽 ( 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )