Definition df-bj-nnbar

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

	Ref	Expression
Assertion	df-bj-nnbar	$$⊢\bar{\mathbb{N}}={\mathbb{N}}_0\cup \left\{+\infty \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnnbar	$$class\bar{\mathbb{N}}$$
1		cn0	$$class{\mathbb{N}}_0$$
2		cpinfty	$$class+\infty$$
3	2	csn	$$class\left\{+\infty \right\}$$
4	1 3	cun	$$class\left({\mathbb{N}}_0\cup \left\{+\infty \right\}\right)$$
5	0 4	wceq	$$wff\bar{\mathbb{N}}={\mathbb{N}}_0\cup \left\{+\infty \right\}$$