Metamath Proof Explorer

Definition df-bj-nnbar

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

Ref Expression
Assertion df-bj-nnbar 
|- NNbar = ( NN0 u. { pinfty } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnnbar 
 |-  NNbar
1 cn0 
 |-  NN0
2 cpinfty 
 |-  pinfty
3 2 csn 
 |-  { pinfty }
4 1 3 cun 
 |-  ( NN0 u. { pinfty } )
5 0 4 wceq 
 |-  NNbar = ( NN0 u. { pinfty } )