Theorem nn0ssxnn0

Description: The standard nonnegative integers are a subset of the extended nonnegative integers. (Contributed by AV, 10-Dec-2020)

	Ref	Expression
Assertion	nn0ssxnn0	$$⊢{\mathbb{N}}_0\subseteq {\mathbb{N}}_0^{*}$$

Proof

Step	Hyp	Ref	Expression
1		ssun1	$$⊢{\mathbb{N}}_0\subseteq {\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
2		df-xnn0	$$⊢{\mathbb{N}}_0^{*}={\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
3	1 2	sseqtrri	$$⊢{\mathbb{N}}_0\subseteq {\mathbb{N}}_0^{*}$$