Definition df-bj-nnbar

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

	Ref	Expression
Assertion	df-bj-nnbar	⊢ ℕ̅ = ( ℕ0 ∪ { +∞ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnnbar	⊢ ℕ̅
1		cn0	⊢ ℕ0
2		cpinfty	⊢ +∞
3	2	csn	⊢ { +∞ }
4	1 3	cun	⊢ ( ℕ0 ∪ { +∞ } )
5	0 4	wceq	⊢ ℕ̅ = ( ℕ0 ∪ { +∞ } )