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 biimtrdi 
 |-  ( ( 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 eqtrid 
 |-  ( ( 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 ) )