Metamath Proof Explorer

Theorem 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 
|- ( ph -> J e. Top )
Assertion sepnsepo 
|- ( ph -> ( E. x e. ( ( nei ` J ) ` C ) E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) <-> E. x e. J E. y e. J ( C C_ x /\ 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 2 sepnsepolem2 
 |-  ( J e. Top -> ( E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) <-> E. y e. J ( D C_ y /\ ( x i^i y ) = (/) ) ) )
4 3 anbi2d 
 |-  ( J e. Top -> ( ( C C_ x /\ E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) ) <-> ( C C_ x /\ E. y e. J ( D C_ y /\ ( x i^i y ) = (/) ) ) ) )
5 4 rexbidv 
 |-  ( J e. Top -> ( E. x e. J ( C C_ x /\ E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) ) <-> E. x e. J ( C C_ x /\ E. y e. J ( D C_ y /\ ( x i^i y ) = (/) ) ) ) )
6 ssrin 
 |-  ( z C_ x -> ( z i^i y ) C_ ( x i^i y ) )
7 sseq0 
 |-  ( ( ( z i^i y ) C_ ( x i^i y ) /\ ( x i^i y ) = (/) ) -> ( z i^i y ) = (/) )
8 7 ex 
 |-  ( ( z i^i y ) C_ ( x i^i y ) -> ( ( x i^i y ) = (/) -> ( z i^i y ) = (/) ) )
9 6 8 syl 
 |-  ( z C_ x -> ( ( x i^i y ) = (/) -> ( z i^i y ) = (/) ) )
10 9 adantl 
 |-  ( ( J e. Top /\ z C_ x ) -> ( ( x i^i y ) = (/) -> ( z i^i y ) = (/) ) )
11 10 reximdv 
 |-  ( ( J e. Top /\ z C_ x ) -> ( E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) -> E. y e. ( ( nei ` J ) ` D ) ( z i^i y ) = (/) ) )
12 simpr 
 |-  ( ( J e. Top /\ x = z ) -> x = z )
13 12 ineq1d 
 |-  ( ( J e. Top /\ x = z ) -> ( x i^i y ) = ( z i^i y ) )
14 13 eqeq1d 
 |-  ( ( J e. Top /\ x = z ) -> ( ( x i^i y ) = (/) <-> ( z i^i y ) = (/) ) )
15 14 rexbidv 
 |-  ( ( J e. Top /\ x = z ) -> ( E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) <-> E. y e. ( ( nei ` J ) ` D ) ( z i^i y ) = (/) ) )
16 2 11 15 opnneieqv 
 |-  ( J e. Top -> ( E. x e. ( ( nei ` J ) ` C ) E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) <-> E. x e. J ( C C_ x /\ E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) ) ) )
17 sepnsepolem1 
 |-  ( E. x e. J E. y e. J ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) <-> E. x e. J ( C C_ x /\ E. y e. J ( D C_ y /\ ( x i^i y ) = (/) ) ) )
18 17 a1i 
 |-  ( J e. Top -> ( E. x e. J E. y e. J ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) <-> E. x e. J ( C C_ x /\ E. y e. J ( D C_ y /\ ( x i^i y ) = (/) ) ) ) )
19 5 16 18 3bitr4d 
 |-  ( J e. Top -> ( E. x e. ( ( nei ` J ) ` C ) E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) <-> E. x e. J E. y e. J ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) ) )
20 1 19 syl 
 |-  ( ph -> ( E. x e. ( ( nei ` J ) ` C ) E. y e. ( ( nei ` J ) ` D ) ( x i^i y ) = (/) <-> E. x e. J E. y e. J ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) ) )