This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-xnn0

Description: Define the set of extended nonnegative integers that includes positive infinity. Analogue of the extension of the real numbers RR* , see df-xr . (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion df-xnn0 ℕ0* = ( ℕ0 ∪ { +∞ } )

Detailed syntax breakdown

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