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 J Top A X A J Clsd J x X y J x y z y z A y A

Proof

Step Hyp Ref Expression
1 isclo.1 X = J
2 1 isclo J Top A X A J Clsd J x X y J x y z y x A z A
3 eleq1w z = w z A w A
4 3 bibi2d z = w x A z A x A w A
5 4 cbvralvw z y x A z A w y x A w A
6 5 anbi2i z y x A z A z y x A z A z y x A z A w y x A w A
7 pm4.24 z y x A z A z y x A z A z y x A z A
8 raaanv z y w y x A z A x A w A z y x A z A w y x A w A
9 6 7 8 3bitr4i z y x A z A z y w y x A z A x A w A
10 bibi1 x A z A x A w A z A w A
11 10 biimpa x A z A x A w A z A w A
12 11 biimpcd z A x A z A x A w A w A
13 12 ralimdv z A w y x A z A x A w A w y w A
14 13 com12 w y x A z A x A w A z A w y w A
15 dfss3 y A w y w A
16 14 15 syl6ibr w y x A z A x A w A z A y A
17 16 ralimi z y w y x A z A x A w A z y z A y A
18 9 17 sylbi z y x A z A z y z A y A
19 eleq1w z = x z A x A
20 19 imbi1d z = x z A y A x A y A
21 20 rspcv x y z y z A y A x A y A
22 dfss3 y A z y z A
23 22 imbi2i x A y A x A z y z A
24 r19.21v z y x A z A x A z y z A
25 23 24 bitr4i x A y A z y x A z A
26 21 25 syl6ib x y z y z A y A z y x A z A
27 ssel y A x y x A
28 27 com12 x y y A x A
29 28 imim2d x y z A y A z A x A
30 29 ralimdv x y z y z A y A z y z A x A
31 26 30 jcad x y z y z A y A z y x A z A z y z A x A
32 ralbiim z y x A z A z y x A z A z y z A x A
33 31 32 syl6ibr x y z y z A y A z y x A z A
34 18 33 impbid2 x y z y x A z A z y z A y A
35 34 pm5.32i x y z y x A z A x y z y z A y A
36 35 rexbii y J x y z y x A z A y J x y z y z A y A
37 36 ralbii x X y J x y z y x A z A x X y J x y z y z A y A
38 2 37 bitrdi J Top A X A J Clsd J x X y J x y z y z A y A