Step |
Hyp |
Ref |
Expression |
1 |
|
restcldi.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
simp2 |
⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) |
3 |
|
dfss |
⊢ ( 𝐵 ⊆ 𝐴 ↔ 𝐵 = ( 𝐵 ∩ 𝐴 ) ) |
4 |
3
|
biimpi |
⊢ ( 𝐵 ⊆ 𝐴 → 𝐵 = ( 𝐵 ∩ 𝐴 ) ) |
5 |
4
|
3ad2ant3 |
⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 = ( 𝐵 ∩ 𝐴 ) ) |
6 |
|
ineq1 |
⊢ ( 𝑣 = 𝐵 → ( 𝑣 ∩ 𝐴 ) = ( 𝐵 ∩ 𝐴 ) ) |
7 |
6
|
rspceeqv |
⊢ ( ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 = ( 𝐵 ∩ 𝐴 ) ) → ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) 𝐵 = ( 𝑣 ∩ 𝐴 ) ) |
8 |
2 5 7
|
syl2anc |
⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) 𝐵 = ( 𝑣 ∩ 𝐴 ) ) |
9 |
|
cldrcl |
⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top ) |
10 |
9
|
3ad2ant2 |
⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐽 ∈ Top ) |
11 |
|
simp1 |
⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐴 ⊆ 𝑋 ) |
12 |
1
|
restcld |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) 𝐵 = ( 𝑣 ∩ 𝐴 ) ) ) |
13 |
10 11 12
|
syl2anc |
⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) 𝐵 = ( 𝑣 ∩ 𝐴 ) ) ) |
14 |
8 13
|
mpbird |
⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ) |