Metamath Proof Explorer

Theorem opnbnd

Description: A set is open iff it is disjoint from its boundary. (Contributed by Jeff Hankins, 23-Sep-2009)

Ref Expression
Hypothesis opnbnd.1 
|- X = U. J
Assertion opnbnd 
|- ( ( J e. Top /\ A C_ X ) -> ( A e. J <-> ( A i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) ) )

Proof

Step Hyp Ref Expression
1 opnbnd.1 
 |-  X = U. J
2 disjdif 
 |-  ( ( ( int ` J ) ` A ) i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/)
3 2 a1i 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( int ` J ) ` A ) i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/) )
4 ineq1 
 |-  ( ( ( int ` J ) ` A ) = A -> ( ( ( int ` J ) ` A ) i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = ( A i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) )
5 4 eqeq1d 
 |-  ( ( ( int ` J ) ` A ) = A -> ( ( ( ( int ` J ) ` A ) i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/) <-> ( A i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/) ) )
6 3 5 syl5ibcom 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( int ` J ) ` A ) = A -> ( A i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/) ) )
7 1 ntrss2 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` A ) C_ A )
8 7 adantr 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( A i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/) ) -> ( ( int ` J ) ` A ) C_ A )
9 inssdif0 
 |-  ( ( A i^i ( ( cls ` J ) ` A ) ) C_ ( ( int ` J ) ` A ) <-> ( A i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/) )
10 1 sscls 
 |-  ( ( J e. Top /\ A C_ X ) -> A C_ ( ( cls ` J ) ` A ) )
11 df-ss 
 |-  ( A C_ ( ( cls ` J ) ` A ) <-> ( A i^i ( ( cls ` J ) ` A ) ) = A )
12 10 11 sylib 
 |-  ( ( J e. Top /\ A C_ X ) -> ( A i^i ( ( cls ` J ) ` A ) ) = A )
13 12 eqcomd 
 |-  ( ( J e. Top /\ A C_ X ) -> A = ( A i^i ( ( cls ` J ) ` A ) ) )
14 eqimss 
 |-  ( A = ( A i^i ( ( cls ` J ) ` A ) ) -> A C_ ( A i^i ( ( cls ` J ) ` A ) ) )
15 13 14 syl 
 |-  ( ( J e. Top /\ A C_ X ) -> A C_ ( A i^i ( ( cls ` J ) ` A ) ) )
16 sstr 
 |-  ( ( A C_ ( A i^i ( ( cls ` J ) ` A ) ) /\ ( A i^i ( ( cls ` J ) ` A ) ) C_ ( ( int ` J ) ` A ) ) -> A C_ ( ( int ` J ) ` A ) )
17 15 16 sylan 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( A i^i ( ( cls ` J ) ` A ) ) C_ ( ( int ` J ) ` A ) ) -> A C_ ( ( int ` J ) ` A ) )
18 9 17 sylan2br 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( A i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/) ) -> A C_ ( ( int ` J ) ` A ) )
19 8 18 eqssd 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( A i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/) ) -> ( ( int ` J ) ` A ) = A )
20 19 ex 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( A i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/) -> ( ( int ` J ) ` A ) = A ) )
21 6 20 impbid 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( int ` J ) ` A ) = A <-> ( A i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/) ) )
22 1 isopn3 
 |-  ( ( J e. Top /\ A C_ X ) -> ( A e. J <-> ( ( int ` J ) ` A ) = A ) )
23 1 topbnd 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) = ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) )
24 23 ineq2d 
 |-  ( ( J e. Top /\ A C_ X ) -> ( A i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = ( A i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) )
25 24 eqeq1d 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( A i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) <-> ( A i^i ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) ) = (/) ) )
26 21 22 25 3bitr4d 
 |-  ( ( J e. Top /\ A C_ X ) -> ( A e. J <-> ( A i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) ) )