Metamath Proof Explorer

Theorem bj-ccssccbar

Description: Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019)

Ref Expression
Assertion bj-ccssccbar 
|- CC C_ CCbar

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  CC C_ ( CC u. CCinfty )
2 df-bj-ccbar 
 |-  CCbar = ( CC u. CCinfty )
3 1 2 sseqtrri 
 |-  CC C_ CCbar