df-bj-nnbar - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-nnbar		Structured version Visualization version GIF version

Definition df-bj-nnbar 35411

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

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

**Detailed syntax breakdown of Definition df-bj-nnbar**
Step	Hyp	Ref	Expression
1		cnnbar 35410	. 2 class ℕ̅
2		cn0 12216	. . 3 class ℕ₀
3		cpinfty 35369	. . . 4 class +∞
4	3	csn 4566	. . 3 class {+∞}
5	2, 4	cun 3889	. 2 class (ℕ₀ ∪ {+∞})
6	1, 5	wceq 1541	1 wff ℕ̅ = (ℕ₀ ∪ {+∞})

Colors of variables: wff setvar class

This definition is referenced by: (None)