Metamath Proof Explorer

Theorem cldbnd

Description: A set is closed iff it contains its boundary. (Contributed by Jeff Hankins, 1-Oct-2009)

Ref Expression
Hypothesis opnbnd.1 ⊢ 𝑋 = ∪ 𝐽
Assertion cldbnd ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 opnbnd.1 ⊢ 𝑋 = ∪ 𝐽
2 1 iscld3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝐴 ) )
3 eqimss ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝐴 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐴 )
4 2 3 syl6bi ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐴 ) )
5 ssinss1 ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐴 → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 )
6 4 5 syl6 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 ) )
7 sslin ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 → ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) ⊆ ( ( 𝑋 ∖ 𝐴 ) ∩ 𝐴 ) )
8 7 adantl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 ) → ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) ⊆ ( ( 𝑋 ∖ 𝐴 ) ∩ 𝐴 ) )
9 incom ⊢ ( ( 𝑋 ∖ 𝐴 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 𝑋 ∖ 𝐴 ) )
10 disjdif ⊢ ( 𝐴 ∩ ( 𝑋 ∖ 𝐴 ) ) = ∅
11 9 10 eqtri ⊢ ( ( 𝑋 ∖ 𝐴 ) ∩ 𝐴 ) = ∅
12 sseq0 ⊢ ( ( ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) ⊆ ( ( 𝑋 ∖ 𝐴 ) ∩ 𝐴 ) ∧ ( ( 𝑋 ∖ 𝐴 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ )
13 8 11 12 sylancl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 ) → ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ )
14 13 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 → ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ ) )
15 incom ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
16 dfss4 ⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 )
17 fveq2 ⊢ ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
18 17 eqcomd ⊢ ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) )
19 16 18 sylbi ⊢ ( 𝐴 ⊆ 𝑋 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) )
20 19 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) )
21 20 ineq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) )
22 15 21 syl5eq ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) )
23 22 ineq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) ) )
24 23 eqeq1d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ ↔ ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) ) = ∅ ) )
25 difss ⊢ ( 𝑋 ∖ 𝐴 ) ⊆ 𝑋
26 1 opnbnd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝐴 ) ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 ↔ ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) ) = ∅ ) )
27 25 26 mpan2 ⊢ ( 𝐽 ∈ Top → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 ↔ ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) ) = ∅ ) )
28 27 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 ↔ ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) ) = ∅ ) )
29 24 28 bitr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ ↔ ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 ) )
30 1 opncld ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) )
31 30 ex ⊢ ( 𝐽 ∈ Top → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 → ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ) )
32 31 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 → ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ) )
33 eleq1 ⊢ ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 → ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ↔ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
34 16 33 sylbi ⊢ ( 𝐴 ⊆ 𝑋 → ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ↔ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
35 34 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ↔ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
36 32 35 sylibd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 → 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
37 29 36 sylbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ → 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
38 14 37 syld ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 → 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
39 6 38 impbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 ) )