Metamath Proof Explorer

Definition df-bj-rrbar

Description: Definition of the set of extended real numbers. This aims to replace df-xr . (Contributed by BJ, 29-Jun-2019)

Ref Expression
Assertion df-bj-rrbar 
|- RRbar = ( RR u. { minfty , pinfty } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crrbar 
 |-  RRbar
1 cr 
 |-  RR
2 cminfty 
 |-  minfty
3 cpinfty 
 |-  pinfty
4 2 3 cpr 
 |-  { minfty , pinfty }
5 1 4 cun 
 |-  ( RR u. { minfty , pinfty } )
6 0 5 wceq 
 |-  RRbar = ( RR u. { minfty , pinfty } )