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 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 syl5eq ( ( 𝐽 ∈ 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 ‘ 𝐽 ) ‘ ( 𝑋𝐴 ) ) ) ⊆ 𝐴 ) )