Theorem sadcl

Description: The sum of two sequences is a sequence. (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Assertion	sadcl	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\mathrm{sadd}B\subseteq {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\subseteq {\mathbb{N}}_0$$
2		simpr	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to B\subseteq {\mathbb{N}}_0$$
3		eqid	$$⊢seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in B,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)=seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in B,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
4	1 2 3	sadfval	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\mathrm{sadd}B=\left\{k\in {\mathbb{N}}_0|hadd\left(k\in A,k\in B,\varnothing \in seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in B,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k\right)\right)\right\}$$
5		ssrab2	$$⊢\left\{k\in {\mathbb{N}}_0|hadd\left(k\in A,k\in B,\varnothing \in seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in B,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k\right)\right)\right\}\subseteq {\mathbb{N}}_0$$
6	4 5	eqsstrdi	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\mathrm{sadd}B\subseteq {\mathbb{N}}_0$$