Definition df-bj-zzbar

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

	Ref	Expression
Assertion	df-bj-zzbar	$$⊢\bar{\mathbb{Z}}=\mathbb{Z}\cup \left\{-\infty ,+\infty \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czzbar	$$class\bar{\mathbb{Z}}$$
1		cz	$$class\mathbb{Z}$$
2		cminfty	$$class-\infty$$
3		cpinfty	$$class+\infty$$
4	2 3	cpr	$$class\left\{-\infty ,+\infty \right\}$$
5	1 4	cun	$$class\left(\mathbb{Z}\cup \left\{-\infty ,+\infty \right\}\right)$$
6	0 5	wceq	$$wff\bar{\mathbb{Z}}=\mathbb{Z}\cup \left\{-\infty ,+\infty \right\}$$