Metamath Proof Explorer

Theorem isclo

Description: A set A is clopen iff for every point x in the space there is a neighborhood y such that all the points in y are in A iff x is. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypothesis isclo.1 ⊢ X = ⋃ J
Assertion isclo ⊢ J ∈ Top ∧ A ⊆ X → A ∈ J ∩ Clsd ⁡ J ↔ ∀ x ∈ X ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A

Proof

Step Hyp Ref Expression
1 isclo.1 ⊢ X = ⋃ J
2 elin ⊢ A ∈ J ∩ Clsd ⁡ J ↔ A ∈ J ∧ A ∈ Clsd ⁡ J
3 1 iscld2 ⊢ J ∈ Top ∧ A ⊆ X → A ∈ Clsd ⁡ J ↔ X ∖ A ∈ J
4 3 anbi2d ⊢ J ∈ Top ∧ A ⊆ X → A ∈ J ∧ A ∈ Clsd ⁡ J ↔ A ∈ J ∧ X ∖ A ∈ J
5 eltop2 ⊢ J ∈ Top → A ∈ J ↔ ∀ x ∈ A ∃ y ∈ J x ∈ y ∧ y ⊆ A
6 dfss3 ⊢ y ⊆ A ↔ ∀ z ∈ y z ∈ A
7 pm5.501 ⊢ x ∈ A → z ∈ A ↔ x ∈ A ↔ z ∈ A
8 7 ralbidv ⊢ x ∈ A → ∀ z ∈ y z ∈ A ↔ ∀ z ∈ y x ∈ A ↔ z ∈ A
9 6 8 syl5bb ⊢ x ∈ A → y ⊆ A ↔ ∀ z ∈ y x ∈ A ↔ z ∈ A
10 9 anbi2d ⊢ x ∈ A → x ∈ y ∧ y ⊆ A ↔ x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
11 10 rexbidv ⊢ x ∈ A → ∃ y ∈ J x ∈ y ∧ y ⊆ A ↔ ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
12 11 ralbiia ⊢ ∀ x ∈ A ∃ y ∈ J x ∈ y ∧ y ⊆ A ↔ ∀ x ∈ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
13 5 12 bitrdi ⊢ J ∈ Top → A ∈ J ↔ ∀ x ∈ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
14 eltop2 ⊢ J ∈ Top → X ∖ A ∈ J ↔ ∀ x ∈ X ∖ A ∃ y ∈ J x ∈ y ∧ y ⊆ X ∖ A
15 dfss3 ⊢ y ⊆ X ∖ A ↔ ∀ z ∈ y z ∈ X ∖ A
16 id ⊢ z ∈ y → z ∈ y
17 simpr ⊢ x ∈ X ∖ A ∧ y ∈ J → y ∈ J
18 elunii ⊢ z ∈ y ∧ y ∈ J → z ∈ ⋃ J
19 16 17 18 syl2anr ⊢ x ∈ X ∖ A ∧ y ∈ J ∧ z ∈ y → z ∈ ⋃ J
20 19 1 eleqtrrdi ⊢ x ∈ X ∖ A ∧ y ∈ J ∧ z ∈ y → z ∈ X
21 eldif ⊢ z ∈ X ∖ A ↔ z ∈ X ∧ ¬ z ∈ A
22 21 baib ⊢ z ∈ X → z ∈ X ∖ A ↔ ¬ z ∈ A
23 20 22 syl ⊢ x ∈ X ∖ A ∧ y ∈ J ∧ z ∈ y → z ∈ X ∖ A ↔ ¬ z ∈ A
24 eldifn ⊢ x ∈ X ∖ A → ¬ x ∈ A
25 nbn2 ⊢ ¬ x ∈ A → ¬ z ∈ A ↔ x ∈ A ↔ z ∈ A
26 24 25 syl ⊢ x ∈ X ∖ A → ¬ z ∈ A ↔ x ∈ A ↔ z ∈ A
27 26 ad2antrr ⊢ x ∈ X ∖ A ∧ y ∈ J ∧ z ∈ y → ¬ z ∈ A ↔ x ∈ A ↔ z ∈ A
28 23 27 bitrd ⊢ x ∈ X ∖ A ∧ y ∈ J ∧ z ∈ y → z ∈ X ∖ A ↔ x ∈ A ↔ z ∈ A
29 28 ralbidva ⊢ x ∈ X ∖ A ∧ y ∈ J → ∀ z ∈ y z ∈ X ∖ A ↔ ∀ z ∈ y x ∈ A ↔ z ∈ A
30 15 29 syl5bb ⊢ x ∈ X ∖ A ∧ y ∈ J → y ⊆ X ∖ A ↔ ∀ z ∈ y x ∈ A ↔ z ∈ A
31 30 anbi2d ⊢ x ∈ X ∖ A ∧ y ∈ J → x ∈ y ∧ y ⊆ X ∖ A ↔ x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
32 31 rexbidva ⊢ x ∈ X ∖ A → ∃ y ∈ J x ∈ y ∧ y ⊆ X ∖ A ↔ ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
33 32 ralbiia ⊢ ∀ x ∈ X ∖ A ∃ y ∈ J x ∈ y ∧ y ⊆ X ∖ A ↔ ∀ x ∈ X ∖ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
34 14 33 bitrdi ⊢ J ∈ Top → X ∖ A ∈ J ↔ ∀ x ∈ X ∖ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
35 13 34 anbi12d ⊢ J ∈ Top → A ∈ J ∧ X ∖ A ∈ J ↔ ∀ x ∈ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A ∧ ∀ x ∈ X ∖ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
36 35 adantr ⊢ J ∈ Top ∧ A ⊆ X → A ∈ J ∧ X ∖ A ∈ J ↔ ∀ x ∈ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A ∧ ∀ x ∈ X ∖ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
37 ralunb ⊢ ∀ x ∈ A ∪ X ∖ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A ↔ ∀ x ∈ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A ∧ ∀ x ∈ X ∖ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
38 simpr ⊢ J ∈ Top ∧ A ⊆ X → A ⊆ X
39 undif ⊢ A ⊆ X ↔ A ∪ X ∖ A = X
40 38 39 sylib ⊢ J ∈ Top ∧ A ⊆ X → A ∪ X ∖ A = X
41 40 raleqdv ⊢ J ∈ Top ∧ A ⊆ X → ∀ x ∈ A ∪ X ∖ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A ↔ ∀ x ∈ X ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
42 37 41 bitr3id ⊢ J ∈ Top ∧ A ⊆ X → ∀ x ∈ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A ∧ ∀ x ∈ X ∖ A ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A ↔ ∀ x ∈ X ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
43 4 36 42 3bitrd ⊢ J ∈ Top ∧ A ⊆ X → A ∈ J ∧ A ∈ Clsd ⁡ J ↔ ∀ x ∈ X ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A
44 2 43 syl5bb ⊢ J ∈ Top ∧ A ⊆ X → A ∈ J ∩ Clsd ⁡ J ↔ ∀ x ∈ X ∃ y ∈ J x ∈ y ∧ ∀ z ∈ y x ∈ A ↔ z ∈ A