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 syl6ibr ( ∀ 𝑤𝑦 ( ( 𝑥𝐴𝑧𝐴 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( 𝑧𝐴𝑦𝐴 ) )
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 syl6ib ( 𝑥𝑦 → ( ∀ 𝑧𝑦 ( 𝑧𝐴𝑦𝐴 ) → ∀ 𝑧𝑦 ( 𝑥𝐴𝑧𝐴 ) ) )
27 ssel ( 𝑦𝐴 → ( 𝑥𝑦𝑥𝐴 ) )
28 27 com12 ( 𝑥𝑦 → ( 𝑦𝐴𝑥𝐴 ) )
29 28 imim2d ( 𝑥𝑦 → ( ( 𝑧𝐴𝑦𝐴 ) → ( 𝑧𝐴𝑥𝐴 ) ) )
30 29 ralimdv ( 𝑥𝑦 → ( ∀ 𝑧𝑦 ( 𝑧𝐴𝑦𝐴 ) → ∀ 𝑧𝑦 ( 𝑧𝐴𝑥𝐴 ) ) )
31 26 30 jcad ( 𝑥𝑦 → ( ∀ 𝑧𝑦 ( 𝑧𝐴𝑦𝐴 ) → ( ∀ 𝑧𝑦 ( 𝑥𝐴𝑧𝐴 ) ∧ ∀ 𝑧𝑦 ( 𝑧𝐴𝑥𝐴 ) ) ) )
32 ralbiim ( ∀ 𝑧𝑦 ( 𝑥𝐴𝑧𝐴 ) ↔ ( ∀ 𝑧𝑦 ( 𝑥𝐴𝑧𝐴 ) ∧ ∀ 𝑧𝑦 ( 𝑧𝐴𝑥𝐴 ) ) )
33 31 32 syl6ibr ( 𝑥𝑦 → ( ∀ 𝑧𝑦 ( 𝑧𝐴𝑦𝐴 ) → ∀ 𝑧𝑦 ( 𝑥𝐴𝑧𝐴 ) ) )
34 18 33 impbid2 ( 𝑥𝑦 → ( ∀ 𝑧𝑦 ( 𝑥𝐴𝑧𝐴 ) ↔ ∀ 𝑧𝑦 ( 𝑧𝐴𝑦𝐴 ) ) )
35 34 pm5.32i ( ( 𝑥𝑦 ∧ ∀ 𝑧𝑦 ( 𝑥𝐴𝑧𝐴 ) ) ↔ ( 𝑥𝑦 ∧ ∀ 𝑧𝑦 ( 𝑧𝐴𝑦𝐴 ) ) )
36 35 rexbii ( ∃ 𝑦𝐽 ( 𝑥𝑦 ∧ ∀ 𝑧𝑦 ( 𝑥𝐴𝑧𝐴 ) ) ↔ ∃ 𝑦𝐽 ( 𝑥𝑦 ∧ ∀ 𝑧𝑦 ( 𝑧𝐴𝑦𝐴 ) ) )
37 36 ralbii ( ∀ 𝑥𝑋𝑦𝐽 ( 𝑥𝑦 ∧ ∀ 𝑧𝑦 ( 𝑥𝐴𝑧𝐴 ) ) ↔ ∀ 𝑥𝑋𝑦𝐽 ( 𝑥𝑦 ∧ ∀ 𝑧𝑦 ( 𝑧𝐴𝑦𝐴 ) ) )
38 2 37 bitrdi ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → ( 𝐴 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ↔ ∀ 𝑥𝑋𝑦𝐽 ( 𝑥𝑦 ∧ ∀ 𝑧𝑦 ( 𝑧𝐴𝑦𝐴 ) ) ) )