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 φ J Top
Assertion sepnsepo φ x nei J C y nei J D x y = x J y J C x D y x y =

Proof

Step Hyp Ref Expression
1 sepnsepolem2.1 φ J Top
2 id J Top J Top
3 2 sepnsepolem2 J Top y nei J D x y = y J D y x y =
4 3 anbi2d J Top C x y nei J D x y = C x y J D y x y =
5 4 rexbidv J Top x J C x y nei J D x y = x J C x y J D y x y =
6 ssrin z x z y x y
7 sseq0 z y x y x y = z y =
8 7 ex z y x y x y = z y =
9 6 8 syl z x x y = z y =
10 9 adantl J Top z x x y = z y =
11 10 reximdv J Top z x y nei J D x y = y nei J D z y =
12 simpr J Top x = z x = z
13 12 ineq1d J Top x = z x y = z y
14 13 eqeq1d J Top x = z x y = z y =
15 14 rexbidv J Top x = z y nei J D x y = y nei J D z y =
16 2 11 15 opnneieqv J Top x nei J C y nei J D x y = x J C x y nei J D x y =
17 sepnsepolem1 x J y J C x D y x y = x J C x y J D y x y =
18 17 a1i J Top x J y J C x D y x y = x J C x y J D y x y =
19 5 16 18 3bitr4d J Top x nei J C y nei J D x y = x J y J C x D y x y =
20 1 19 syl φ x nei J C y nei J D x y = x J y J C x D y x y =