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 incom 
 |-  ( ( X \ A ) i^i A ) = ( A i^i ( X \ A ) )
10 disjdif 
 |-  ( A i^i ( X \ A ) ) = (/)
11 9 10 eqtri 
 |-  ( ( X \ A ) i^i A ) = (/)
12 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 ) ) ) ) = (/) )
13 8 11 12 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 ) ) ) ) = (/) )
14 13 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 ) ) ) ) = (/) ) )
15 incom 
 |-  ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) = ( ( ( cls ` J ) ` ( X \ A ) ) i^i ( ( cls ` J ) ` A ) )
16 dfss4 
 |-  ( A C_ X <-> ( X \ ( X \ A ) ) = A )
17 fveq2 
 |-  ( ( X \ ( X \ A ) ) = A -> ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) = ( ( cls ` J ) ` A ) )
18 17 eqcomd 
 |-  ( ( X \ ( X \ A ) ) = A -> ( ( cls ` J ) ` A ) = ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) )
19 16 18 sylbi 
 |-  ( A C_ X -> ( ( cls ` J ) ` A ) = ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) )
20 19 adantl 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` A ) = ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) )
21 20 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 ) ) ) ) )
22 15 21 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 ) ) ) ) )
23 22 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 ) ) ) ) ) )
24 23 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 ) ) ) ) ) = (/) ) )
25 difss 
 |-  ( X \ A ) C_ X
26 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 ) ) ) ) ) = (/) ) )
27 25 26 mpan2 
 |-  ( J e. Top -> ( ( X \ A ) e. J <-> ( ( X \ A ) i^i ( ( ( cls ` J ) ` ( X \ A ) ) i^i ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) ) = (/) ) )
28 27 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 ) ) ) ) ) = (/) ) )
29 24 28 bitr4d 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) <-> ( X \ A ) e. J ) )
30 1 opncld 
 |-  ( ( J e. Top /\ ( X \ A ) e. J ) -> ( X \ ( X \ A ) ) e. ( Clsd ` J ) )
31 30 ex 
 |-  ( J e. Top -> ( ( X \ A ) e. J -> ( X \ ( X \ A ) ) e. ( Clsd ` J ) ) )
32 31 adantr 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( X \ A ) e. J -> ( X \ ( X \ A ) ) e. ( Clsd ` J ) ) )
33 eleq1 
 |-  ( ( X \ ( X \ A ) ) = A -> ( ( X \ ( X \ A ) ) e. ( Clsd ` J ) <-> A e. ( Clsd ` J ) ) )
34 16 33 sylbi 
 |-  ( A C_ X -> ( ( X \ ( X \ A ) ) e. ( Clsd ` J ) <-> A e. ( Clsd ` J ) ) )
35 34 adantl 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( X \ ( X \ A ) ) e. ( Clsd ` J ) <-> A e. ( Clsd ` J ) ) )
36 32 35 sylibd 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( X \ A ) e. J -> A e. ( Clsd ` J ) ) )
37 29 36 sylbid 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( X \ A ) i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) -> A e. ( Clsd ` J ) ) )
38 14 37 syld 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A -> A e. ( Clsd ` J ) ) )
39 6 38 impbid 
 |-  ( ( J e. Top /\ A C_ X ) -> ( A e. ( Clsd ` J ) <-> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A ) )