Definition df-bj-zzhat

Description: Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023)

	Ref	Expression
Assertion	df-bj-zzhat	$$⊢\hat{\mathbb{Z}}=\mathbb{Z}\cup \left\{\infty \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czzhat	$$class\hat{\mathbb{Z}}$$
1		cz	$$class\mathbb{Z}$$
2		cinfty	$$class\infty$$
3	2	csn	$$class\left\{\infty \right\}$$
4	1 3	cun	$$class\left(\mathbb{Z}\cup \left\{\infty \right\}\right)$$
5	0 4	wceq	$$wff\hat{\mathbb{Z}}=\mathbb{Z}\cup \left\{\infty \right\}$$