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 ⊢ 𝑋 = ∪ 𝐽
Assertion isclo ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) ) )

Proof

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