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 biimtrdi ⊢ ( ( 𝐽 ∈ 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 disjdifr ⊢ ( ( 𝑋 ∖ 𝐴 ) ∩ 𝐴 ) = ∅
10 sseq0 ⊢ ( ( ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) ⊆ ( ( 𝑋 ∖ 𝐴 ) ∩ 𝐴 ) ∧ ( ( 𝑋 ∖ 𝐴 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ )
11 8 9 10 sylancl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 ) → ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ )
12 11 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 → ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ ) )
13 incom ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
14 dfss4 ⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 )
15 fveq2 ⊢ ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
16 15 eqcomd ⊢ ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) )
17 14 16 sylbi ⊢ ( 𝐴 ⊆ 𝑋 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) )
18 17 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) )
19 18 ineq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) )
20 13 19 eqtrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) )
21 20 ineq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) ) )
22 21 eqeq1d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ ↔ ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) ) = ∅ ) )
23 difss ⊢ ( 𝑋 ∖ 𝐴 ) ⊆ 𝑋
24 1 opnbnd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝐴 ) ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 ↔ ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) ) = ∅ ) )
25 23 24 mpan2 ⊢ ( 𝐽 ∈ Top → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 ↔ ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) ) = ∅ ) )
26 25 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 ↔ ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) ) = ∅ ) )
27 22 26 bitr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ ↔ ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 ) )
28 1 opncld ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) )
29 28 ex ⊢ ( 𝐽 ∈ Top → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 → ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ) )
30 29 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 → ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ) )
31 eleq1 ⊢ ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 → ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ↔ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
32 14 31 sylbi ⊢ ( 𝐴 ⊆ 𝑋 → ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ↔ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
33 32 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ↔ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
34 30 33 sylibd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝐴 ) ∈ 𝐽 → 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
35 27 34 sylbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( 𝑋 ∖ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ → 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
36 12 35 syld ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 → 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
37 6 36 impbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ⊆ 𝐴 ) )