Metamath Proof Explorer

Theorem cnfldtop

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

Ref Expression
Hypothesis cnfldtopn.1 
|- J = ( TopOpen ` CCfld )
Assertion cnfldtop 
|- J e. Top

Proof

Step Hyp Ref Expression
1 cnfldtopn.1 
 |-  J = ( TopOpen ` CCfld )
2 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
3 2 topontopi 
 |-  J e. Top