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	|- ( ph -> J e. Top )
Assertion	sepnsepolem2	|- ( ph -> ( E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) <-> E. y e. J ( D C_ y /\ ( x i^i y ) = (/) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sepnsepolem2.1	|- ( ph -> J e. Top )
2		id	|- ( J e. Top -> J e. Top )
3		sslin	|- ( z C_ y -> ( x i^i z ) C_ ( x i^i y ) )
4		sseq0	|- ( ( ( x i^i z ) C_ ( x i^i y ) /\ ( x i^i y ) = (/) ) -> ( x i^i z ) = (/) )
5	4	ex	|- ( ( x i^i z ) C_ ( x i^i y ) -> ( ( x i^i y ) = (/) -> ( x i^i z ) = (/) ) )
6	3 5	syl	|- ( z C_ y -> ( ( x i^i y ) = (/) -> ( x i^i z ) = (/) ) )
7	6	adantl	|- ( ( J e. Top /\ z C_ y ) -> ( ( x i^i y ) = (/) -> ( x i^i z ) = (/) ) )
8		ineq2	|- ( y = z -> ( x i^i y ) = ( x i^i z ) )
9	8	eqeq1d	|- ( y = z -> ( ( x i^i y ) = (/) <-> ( x i^i z ) = (/) ) )
10	9	adantl	|- ( ( J e. Top /\ y = z ) -> ( ( x i^i y ) = (/) <-> ( x i^i z ) = (/) ) )
11	2 7 10	opnneieqv	|- ( J e. Top -> ( E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) <-> E. y e. J ( D C_ y /\ ( x i^i y ) = (/) ) ) )
12	1 11	syl	|- ( ph -> ( E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) <-> E. y e. J ( D C_ y /\ ( x i^i y ) = (/) ) ) )