Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Zhi Wang
Topology
Separated spaces: T0, T1, T2 (Hausdorff) ...
iscnrm3rlem5
Next ⟩
iscnrm3rlem6
Metamath Proof Explorer
Ascii
Unicode
Theorem
iscnrm3rlem5
Description:
Lemma for
iscnrm3rlem6
.
(Contributed by
Zhi Wang
, 5-Sep-2024)
Ref
Expression
Hypotheses
iscnrm3rlem4.1
⊢
φ
→
J
∈
Top
iscnrm3rlem4.2
⊢
φ
→
S
⊆
⋃
J
iscnrm3rlem5.3
⊢
φ
→
T
⊆
⋃
J
Assertion
iscnrm3rlem5
⊢
φ
→
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
∈
J
Proof
Step
Hyp
Ref
Expression
1
iscnrm3rlem4.1
⊢
φ
→
J
∈
Top
2
iscnrm3rlem4.2
⊢
φ
→
S
⊆
⋃
J
3
iscnrm3rlem5.3
⊢
φ
→
T
⊆
⋃
J
4
eqid
⊢
⋃
J
=
⋃
J
5
4
clscld
⊢
J
∈
Top
∧
S
⊆
⋃
J
→
cls
⁡
J
⁡
S
∈
Clsd
⁡
J
6
1
2
5
syl2anc
⊢
φ
→
cls
⁡
J
⁡
S
∈
Clsd
⁡
J
7
4
clscld
⊢
J
∈
Top
∧
T
⊆
⋃
J
→
cls
⁡
J
⁡
T
∈
Clsd
⁡
J
8
1
3
7
syl2anc
⊢
φ
→
cls
⁡
J
⁡
T
∈
Clsd
⁡
J
9
incld
⊢
cls
⁡
J
⁡
S
∈
Clsd
⁡
J
∧
cls
⁡
J
⁡
T
∈
Clsd
⁡
J
→
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
∈
Clsd
⁡
J
10
6
8
9
syl2anc
⊢
φ
→
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
∈
Clsd
⁡
J
11
4
cldopn
⊢
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
∈
Clsd
⁡
J
→
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
∈
J
12
10
11
syl
⊢
φ
→
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
∈
J