Definition df-bj-zzbar

Description: Definition of the extended integers. (Contributed by BJ, 28-Jul-2023)

	Ref	Expression
Assertion	df-bj-zzbar	⊢ ℤ̅ = ( ℤ ∪ { -∞ , +∞ } )

Detailed syntax breakdown

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