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	⊢ ℕ0 ⊆ ℕ0*

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ ℕ0 ⊆ ( ℕ0 ∪ { +∞ } )
2		df-xnn0	⊢ ℕ0* = ( ℕ0 ∪ { +∞ } )
3	1 2	sseqtrri	⊢ ℕ0 ⊆ ℕ0*