Definition df-bj-zzbar

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

	Ref	Expression
Assertion	df-bj-zzbar	|- ZZbar = ( ZZ u. { minfty , pinfty } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czzbar	|- ZZbar
1		cz	|- ZZ
2		cminfty	|- minfty
3		cpinfty	|- pinfty
4	2 3	cpr	|- { minfty , pinfty }
5	1 4	cun	|- ( ZZ u. { minfty , pinfty } )
6	0 5	wceq	|- ZZbar = ( ZZ u. { minfty , pinfty } )