Metamath Proof Explorer

Theorem bj-ccinftyssccbar

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

Ref Expression
Assertion bj-ccinftyssccbar 
|- CCinfty C_ CCbar

Proof

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