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
|- X = U. J
Assertion cldbnd
|- ( ( J e. Top /\ A C_ X ) -> ( A e. ( Clsd ` J ) <-> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A ) )

Proof

Step Hyp Ref Expression
1 opnbnd.1
 |-  X = U. J
2 1 iscld3
 |-  ( ( J e. Top /\ A C_ X ) -> ( A e. ( Clsd ` J ) <-> ( ( cls ` J ) ` A ) = A ) )
3 eqimss
 |-  ( ( ( cls ` J ) ` A ) = A -> ( ( cls ` J ) ` A ) C_ A )
4 2 3 syl6bi
 |-  ( ( J e. Top /\ A C_ X ) -> ( A e. ( Clsd ` J ) -> ( ( cls ` J ) ` A ) C_ A ) )
5 ssinss1
 |-  ( ( ( cls ` J ) ` A ) C_ A -> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A )
6 4 5 syl6
 |-  ( ( J e. Top /\ A C_ X ) -> ( A e. ( Clsd ` J ) -> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A ) )
7 sslin
 |-  ( ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A -> ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) C_ ( ( X \ A ) i^i A ) )
8 7 adantl
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A ) -> ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) C_ ( ( X \ A ) i^i A ) )
9 disjdifr
 |-  ( ( X \ A ) i^i A ) = (/)
10 sseq0
 |-  ( ( ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) C_ ( ( X \ A ) i^i A ) /\ ( ( X \ A ) i^i A ) = (/) ) -> ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) )
11 8 9 10 sylancl
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A ) -> ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) )
12 11 ex
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A -> ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) ) )
13 incom
 |-  ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) = ( ( ( cls ` J ) ` ( X \ A ) ) i^i ( ( cls ` J ) ` A ) )
14 dfss4
 |-  ( A C_ X <-> ( X \ ( X \ A ) ) = A )
15 fveq2
 |-  ( ( X \ ( X \ A ) ) = A -> ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) = ( ( cls ` J ) ` A ) )
16 15 eqcomd
 |-  ( ( X \ ( X \ A ) ) = A -> ( ( cls ` J ) ` A ) = ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) )
17 14 16 sylbi
 |-  ( A C_ X -> ( ( cls ` J ) ` A ) = ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) )
18 17 adantl
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` A ) = ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) )
19 18 ineq2d
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` ( X \ A ) ) i^i ( ( cls ` J ) ` A ) ) = ( ( ( cls ` J ) ` ( X \ A ) ) i^i ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) )
20 13 19 syl5eq
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) = ( ( ( cls ` J ) ` ( X \ A ) ) i^i ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) )
21 20 ineq2d
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = ( ( X \ A ) i^i ( ( ( cls ` J ) ` ( X \ A ) ) i^i ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) ) )
22 21 eqeq1d
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) <-> ( ( X \ A ) i^i ( ( ( cls ` J ) ` ( X \ A ) ) i^i ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) ) = (/) ) )
23 difss
 |-  ( X \ A ) C_ X
24 1 opnbnd
 |-  ( ( J e. Top /\ ( X \ A ) C_ X ) -> ( ( X \ A ) e. J <-> ( ( X \ A ) i^i ( ( ( cls ` J ) ` ( X \ A ) ) i^i ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) ) = (/) ) )
25 23 24 mpan2
 |-  ( J e. Top -> ( ( X \ A ) e. J <-> ( ( X \ A ) i^i ( ( ( cls ` J ) ` ( X \ A ) ) i^i ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) ) = (/) ) )
26 25 adantr
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( X \ A ) e. J <-> ( ( X \ A ) i^i ( ( ( cls ` J ) ` ( X \ A ) ) i^i ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) ) = (/) ) )
27 22 26 bitr4d
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) <-> ( X \ A ) e. J ) )
28 1 opncld
 |-  ( ( J e. Top /\ ( X \ A ) e. J ) -> ( X \ ( X \ A ) ) e. ( Clsd ` J ) )
29 28 ex
 |-  ( J e. Top -> ( ( X \ A ) e. J -> ( X \ ( X \ A ) ) e. ( Clsd ` J ) ) )
30 29 adantr
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( X \ A ) e. J -> ( X \ ( X \ A ) ) e. ( Clsd ` J ) ) )
31 eleq1
 |-  ( ( X \ ( X \ A ) ) = A -> ( ( X \ ( X \ A ) ) e. ( Clsd ` J ) <-> A e. ( Clsd ` J ) ) )
32 14 31 sylbi
 |-  ( A C_ X -> ( ( X \ ( X \ A ) ) e. ( Clsd ` J ) <-> A e. ( Clsd ` J ) ) )
33 32 adantl
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( X \ ( X \ A ) ) e. ( Clsd ` J ) <-> A e. ( Clsd ` J ) ) )
34 30 33 sylibd
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( X \ A ) e. J -> A e. ( Clsd ` J ) ) )
35 27 34 sylbid
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) -> A e. ( Clsd ` J ) ) )
36 12 35 syld
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A -> A e. ( Clsd ` J ) ) )
37 6 36 impbid
 |-  ( ( J e. Top /\ A C_ X ) -> ( A e. ( Clsd ` J ) <-> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A ) )