Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Zhi Wang
Topology
Subspace topologies
restclsseplem
Next ⟩
restclssep
Metamath Proof Explorer
Ascii
Unicode
Theorem
restclsseplem
Description:
Lemma for
restclssep
.
(Contributed by
Zhi Wang
, 2-Sep-2024)
Ref
Expression
Hypotheses
restcls2.1
⊢
φ
→
J
∈
Top
restcls2.2
⊢
φ
→
X
=
⋃
J
restcls2.3
⊢
φ
→
Y
⊆
X
restcls2.4
⊢
φ
→
K
=
J
↾
𝑡
Y
restcls2.5
⊢
φ
→
S
∈
Clsd
⁡
K
restclsseplem.6
⊢
φ
→
S
∩
T
=
∅
restclsseplem.7
⊢
φ
→
T
⊆
Y
Assertion
restclsseplem
⊢
φ
→
cls
⁡
J
⁡
S
∩
T
=
∅
Proof
Step
Hyp
Ref
Expression
1
restcls2.1
⊢
φ
→
J
∈
Top
2
restcls2.2
⊢
φ
→
X
=
⋃
J
3
restcls2.3
⊢
φ
→
Y
⊆
X
4
restcls2.4
⊢
φ
→
K
=
J
↾
𝑡
Y
5
restcls2.5
⊢
φ
→
S
∈
Clsd
⁡
K
6
restclsseplem.6
⊢
φ
→
S
∩
T
=
∅
7
restclsseplem.7
⊢
φ
→
T
⊆
Y
8
1
2
3
4
5
restcls2
⊢
φ
→
S
=
cls
⁡
J
⁡
S
∩
Y
9
8
ineq1d
⊢
φ
→
S
∩
T
=
cls
⁡
J
⁡
S
∩
Y
∩
T
10
inass
⊢
cls
⁡
J
⁡
S
∩
Y
∩
T
=
cls
⁡
J
⁡
S
∩
Y
∩
T
11
9
10
eqtrdi
⊢
φ
→
S
∩
T
=
cls
⁡
J
⁡
S
∩
Y
∩
T
12
sseqin2
⊢
T
⊆
Y
↔
Y
∩
T
=
T
13
7
12
sylib
⊢
φ
→
Y
∩
T
=
T
14
13
ineq2d
⊢
φ
→
cls
⁡
J
⁡
S
∩
Y
∩
T
=
cls
⁡
J
⁡
S
∩
T
15
11
6
14
3eqtr3rd
⊢
φ
→
cls
⁡
J
⁡
S
∩
T
=
∅