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 ⊢ 𝑋 = ∪ 𝐽
Assertion opnbnd ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ 𝐽 ↔ ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 opnbnd.1 ⊢ 𝑋 = ∪ 𝐽
2 disjdif ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅
3 2 a1i ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅ )
4 ineq1 ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) = 𝐴 → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) )
5 4 eqeq1d ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) = 𝐴 → ( ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅ ↔ ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅ ) )
6 3 5 syl5ibcom ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) = 𝐴 → ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅ ) )
7 1 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐴 )
8 7 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅ ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐴 )
9 inssdif0 ⊢ ( ( 𝐴 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅ )
10 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
11 dfss2 ⊢ ( 𝐴 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( 𝐴 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 )
12 10 11 sylib ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 )
13 12 eqcomd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 = ( 𝐴 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
14 eqimss ⊢ ( 𝐴 = ( 𝐴 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐴 ⊆ ( 𝐴 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
15 13 14 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ ( 𝐴 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
16 sstr ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ∧ ( 𝐴 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐴 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
17 15 16 sylan ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐴 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
18 9 17 sylan2br ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅ ) → 𝐴 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
19 8 18 eqssd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅ ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) = 𝐴 )
20 19 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅ → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) = 𝐴 ) )
21 6 20 impbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅ ) )
22 1 isopn3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) = 𝐴 ) )
23 1 topbnd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
24 23 ineq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) )
25 24 eqeq1d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ ↔ ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ∅ ) )
26 21 22 25 3bitr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ 𝐽 ↔ ( 𝐴 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) = ∅ ) )