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	⊢ ℝ̅ = ( ℝ ∪ { -∞ , +∞ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrbar	⊢ ℝ̅
1		cr	⊢ ℝ
2		cminfty	⊢ -∞
3		cpinfty	⊢ +∞
4	2 3	cpr	⊢ { -∞ , +∞ }
5	1 4	cun	⊢ ( ℝ ∪ { -∞ , +∞ } )
6	0 5	wceq	⊢ ℝ̅ = ( ℝ ∪ { -∞ , +∞ } )