Theorem sadid2

Description: The adder sequence function has a right identity, the empty set, which is the representation of the integer zero. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Assertion	sadid2	$$⊢A\subseteq {\mathbb{N}}_0\to \varnothing \mathrm{sadd}A=A$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq {\mathbb{N}}_0$$
2		sadcom	$$⊢\left(\varnothing \subseteq {\mathbb{N}}_0\wedge A\subseteq {\mathbb{N}}_0\right)\to \varnothing \mathrm{sadd}A=A\mathrm{sadd}\varnothing$$
3	1 2	mpan	$$⊢A\subseteq {\mathbb{N}}_0\to \varnothing \mathrm{sadd}A=A\mathrm{sadd}\varnothing$$
4		sadid1	$$⊢A\subseteq {\mathbb{N}}_0\to A\mathrm{sadd}\varnothing =A$$
5	3 4	eqtrd	$$⊢A\subseteq {\mathbb{N}}_0\to \varnothing \mathrm{sadd}A=A$$