Definition df-bj-zzhat

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

	Ref	Expression
Assertion	df-bj-zzhat	⊢ ℤ̂ = ( ℤ ∪ { ∞ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czzhat	⊢ ℤ̂
1		cz	⊢ ℤ
2		cinfty	⊢ ∞
3	2	csn	⊢ { ∞ }
4	1 3	cun	⊢ ( ℤ ∪ { ∞ } )
5	0 4	wceq	⊢ ℤ̂ = ( ℤ ∪ { ∞ } )