Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Zhi Wang
Topology
Separated spaces: T0, T1, T2 (Hausdorff) ...
iscnrm3rlem6
Next ⟩
iscnrm3rlem7
Metamath Proof Explorer
Ascii
Unicode
Theorem
iscnrm3rlem6
Description:
Lemma for
iscnrm3rlem7
.
(Contributed by
Zhi Wang
, 5-Sep-2024)
Ref
Expression
Hypotheses
iscnrm3rlem4.1
⊢
φ
→
J
∈
Top
iscnrm3rlem4.2
⊢
φ
→
S
⊆
⋃
J
iscnrm3rlem5.3
⊢
φ
→
T
⊆
⋃
J
iscnrm3rlem6.4
⊢
φ
→
O
⊆
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
Assertion
iscnrm3rlem6
⊢
φ
→
O
∈
J
↾
𝑡
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
↔
O
∈
J
Proof
Step
Hyp
Ref
Expression
1
iscnrm3rlem4.1
⊢
φ
→
J
∈
Top
2
iscnrm3rlem4.2
⊢
φ
→
S
⊆
⋃
J
3
iscnrm3rlem5.3
⊢
φ
→
T
⊆
⋃
J
4
iscnrm3rlem6.4
⊢
φ
→
O
⊆
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
5
1
2
3
iscnrm3rlem5
⊢
φ
→
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
∈
J
6
restopn2
⊢
J
∈
Top
∧
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
∈
J
→
O
∈
J
↾
𝑡
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
↔
O
∈
J
∧
O
⊆
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
7
1
5
6
syl2anc
⊢
φ
→
O
∈
J
↾
𝑡
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
↔
O
∈
J
∧
O
⊆
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
8
4
7
mpbiran2d
⊢
φ
→
O
∈
J
↾
𝑡
⋃
J
∖
cls
⁡
J
⁡
S
∩
cls
⁡
J
⁡
T
↔
O
∈
J