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

Proof

Step Hyp Ref Expression
1 isclo.1 ⊢ 𝑋 = ∪ 𝐽
2 1 isclo ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) ) )
3 eleq1w ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
4 3 bibi2d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) )
5 4 cbvralvw ⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ↔ ∀ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
6 5 anbi2i ⊢ ( ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) ↔ ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) )
7 pm4.24 ⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ↔ ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) )
8 raaanv ⊢ ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) ↔ ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) )
9 6 7 8 3bitr4i ⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ↔ ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) )
10 bibi1 ⊢ ( ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ↔ ( 𝑧 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) )
11 10 biimpa ⊢ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
12 11 biimpcd ⊢ ( 𝑧 ∈ 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) → 𝑤 ∈ 𝐴 ) )
13 12 ralimdv ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑤 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) → ∀ 𝑤 ∈ 𝑦 𝑤 ∈ 𝐴 ) )
14 13 com12 ⊢ ( ∀ 𝑤 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 ∈ 𝐴 → ∀ 𝑤 ∈ 𝑦 𝑤 ∈ 𝐴 ) )
15 dfss3 ⊢ ( 𝑦 ⊆ 𝐴 ↔ ∀ 𝑤 ∈ 𝑦 𝑤 ∈ 𝐴 )
16 14 15 imbitrrdi ⊢ ( ∀ 𝑤 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) )
17 16 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) → ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) )
18 9 17 sylbi ⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) → ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) )
19 eleq1w ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
20 19 imbi1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) ) )
21 20 rspcv ⊢ ( 𝑥 ∈ 𝑦 → ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) ) )
22 dfss3 ⊢ ( 𝑦 ⊆ 𝐴 ↔ ∀ 𝑧 ∈ 𝑦 𝑧 ∈ 𝐴 )
23 22 imbi2i ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ∈ 𝑦 𝑧 ∈ 𝐴 ) )
24 r19.21v ⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ∈ 𝑦 𝑧 ∈ 𝐴 ) )
25 23 24 bitr4i ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) ↔ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) )
26 21 25 imbitrdi ⊢ ( 𝑥 ∈ 𝑦 → ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) → ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) )
27 ssel ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ 𝐴 ) )
28 27 com12 ⊢ ( 𝑥 ∈ 𝑦 → ( 𝑦 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) )
29 28 imim2d ⊢ ( 𝑥 ∈ 𝑦 → ( ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) → ( 𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴 ) ) )
30 29 ralimdv ⊢ ( 𝑥 ∈ 𝑦 → ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) → ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴 ) ) )
31 26 30 jcad ⊢ ( 𝑥 ∈ 𝑦 → ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) → ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴 ) ) ) )
32 ralbiim ⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ↔ ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴 ) ) )
33 31 32 imbitrrdi ⊢ ( 𝑥 ∈ 𝑦 → ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) → ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) )
34 18 33 impbid2 ⊢ ( 𝑥 ∈ 𝑦 → ( ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ↔ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) ) )
35 34 pm5.32i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) ) )
36 35 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) ) )
37 36 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) ) )
38 2 37 bitrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴 ) ) ) )