Step |
Hyp |
Ref |
Expression |
1 |
|
topbnd.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
1
|
clsdif |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) |
3 |
2
|
ineq2d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) ) |
4 |
|
indif2 |
⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) = ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ 𝑋 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) |
5 |
3 4
|
eqtrdi |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ 𝑋 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) |
6 |
1
|
clsss3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 ) |
7 |
|
df-ss |
⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ 𝑋 ) = ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) |
8 |
6 7
|
sylib |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ 𝑋 ) = ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) |
9 |
8
|
difeq1d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ 𝑋 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) |
10 |
5 9
|
eqtrd |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) |