Metamath Proof Explorer

Theorem cnfldtopon

Description: The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypothesis cnfldtopn.1 J = TopOpen fld
Assertion cnfldtopon J TopOn


Step Hyp Ref Expression
1 cnfldtopn.1 J = TopOpen fld
2 cnfldtps fld TopSp
3 cnfldbas = Base fld
4 3 1 istps fld TopSp J TopOn
5 2 4 mpbi J TopOn