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 = J
Assertion opnbnd J Top A X A J A cls J A cls J X A =

Proof

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