Metamath Proof Explorer

Definition df-bj-zzhat

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

Ref Expression
Assertion df-bj-zzhat 
|- ZZhat = ( ZZ u. { infty } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 czzhat 
 |-  ZZhat
1 cz 
 |-  ZZ
2 cinfty 
 |-  infty
3 2 csn 
 |-  { infty }
4 1 3 cun 
 |-  ( ZZ u. { infty } )
5 0 4 wceq 
 |-  ZZhat = ( ZZ u. { infty } )