Metamath Proof Explorer


Theorem isclo2

Description: A set A is clopen iff for every point x in the space there is a neighborhood y of x which is either disjoint from A or contained in A . (Contributed by Mario Carneiro, 7-Jul-2015)

Ref Expression
Hypothesis isclo.1 X=J
Assertion isclo2 JTopAXAJClsdJxXyJxyzyzAyA

Proof

Step Hyp Ref Expression
1 isclo.1 X=J
2 1 isclo JTopAXAJClsdJxXyJxyzyxAzA
3 eleq1w z=wzAwA
4 3 bibi2d z=wxAzAxAwA
5 4 cbvralvw zyxAzAwyxAwA
6 5 anbi2i zyxAzAzyxAzAzyxAzAwyxAwA
7 pm4.24 zyxAzAzyxAzAzyxAzA
8 raaanv zywyxAzAxAwAzyxAzAwyxAwA
9 6 7 8 3bitr4i zyxAzAzywyxAzAxAwA
10 bibi1 xAzAxAwAzAwA
11 10 biimpa xAzAxAwAzAwA
12 11 biimpcd zAxAzAxAwAwA
13 12 ralimdv zAwyxAzAxAwAwywA
14 13 com12 wyxAzAxAwAzAwywA
15 dfss3 yAwywA
16 14 15 syl6ibr wyxAzAxAwAzAyA
17 16 ralimi zywyxAzAxAwAzyzAyA
18 9 17 sylbi zyxAzAzyzAyA
19 eleq1w z=xzAxA
20 19 imbi1d z=xzAyAxAyA
21 20 rspcv xyzyzAyAxAyA
22 dfss3 yAzyzA
23 22 imbi2i xAyAxAzyzA
24 r19.21v zyxAzAxAzyzA
25 23 24 bitr4i xAyAzyxAzA
26 21 25 imbitrdi xyzyzAyAzyxAzA
27 ssel yAxyxA
28 27 com12 xyyAxA
29 28 imim2d xyzAyAzAxA
30 29 ralimdv xyzyzAyAzyzAxA
31 26 30 jcad xyzyzAyAzyxAzAzyzAxA
32 ralbiim zyxAzAzyxAzAzyzAxA
33 31 32 syl6ibr xyzyzAyAzyxAzA
34 18 33 impbid2 xyzyxAzAzyzAyA
35 34 pm5.32i xyzyxAzAxyzyzAyA
36 35 rexbii yJxyzyxAzAyJxyzyzAyA
37 36 ralbii xXyJxyzyxAzAxXyJxyzyzAyA
38 2 37 bitrdi JTopAXAJClsdJxXyJxyzyzAyA