Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Chen-Pang He
Ordinal topology
ordtopt0
Next ⟩
onsucsuccmpi
Metamath Proof Explorer
Ascii
Unicode
Theorem
ordtopt0
Description:
An ordinal topology is T_0.
(Contributed by
Chen-Pang He
, 8-Nov-2015)
Ref
Expression
Assertion
ordtopt0
⊢
Ord
⁡
J
→
J
∈
Top
↔
J
∈
Kol2
Proof
Step
Hyp
Ref
Expression
1
ordtop
⊢
Ord
⁡
J
→
J
∈
Top
↔
J
≠
⋃
J
2
onsuct0
⊢
⋃
J
∈
On
→
suc
⁡
⋃
J
∈
Kol2
3
2
ordtoplem
⊢
Ord
⁡
J
→
J
≠
⋃
J
→
J
∈
Kol2
4
1
3
sylbid
⊢
Ord
⁡
J
→
J
∈
Top
→
J
∈
Kol2
5
t0top
⊢
J
∈
Kol2
→
J
∈
Top
6
4
5
impbid1
⊢
Ord
⁡
J
→
J
∈
Top
↔
J
∈
Kol2