Theorem saddisj

Description: The sum of disjoint sequences is the union of the sequences. (In this case, there are no carried bits.) (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	saddisj.1	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
	saddisj.2	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
	saddisj.3	$$⊢\phi \to A\cap B=\varnothing$$
Assertion	saddisj	$$⊢\phi \to A\mathrm{sadd}B=A\cup B$$

Proof

Step	Hyp	Ref	Expression
1		saddisj.1	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		saddisj.2	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		saddisj.3	$$⊢\phi \to A\cap B=\varnothing$$
4		sadcl	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\mathrm{sadd}B\subseteq {\mathbb{N}}_0$$
5	1 2 4	syl2anc	$$⊢\phi \to A\mathrm{sadd}B\subseteq {\mathbb{N}}_0$$
6	5	sseld	$$⊢\phi \to \left(k\in \left(A\mathrm{sadd}B\right)\to k\in {\mathbb{N}}_0\right)$$
7	1 2	unssd	$$⊢\phi \to A\cup B\subseteq {\mathbb{N}}_0$$
8	7	sseld	$$⊢\phi \to \left(k\in \left(A\cup B\right)\to k\in {\mathbb{N}}_0\right)$$
9	1	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\subseteq {\mathbb{N}}_0$$
10	2	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to B\subseteq {\mathbb{N}}_0$$
11	3	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\cap B=\varnothing$$
12		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(x\in {\mathbb{N}}_0⟼if\left(x=0,\varnothing ,x-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(x\in {\mathbb{N}}_0⟼if\left(x=0,\varnothing ,x-1\right)\right)\right)$$
13		simpr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\in {\mathbb{N}}_0$$
14	9 10 11 12 13	saddisjlem	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(k\in \left(A\mathrm{sadd}B\right)\leftrightarrow k\in \left(A\cup B\right)\right)$$
15	14	ex	$$⊢\phi \to \left(k\in {\mathbb{N}}_0\to \left(k\in \left(A\mathrm{sadd}B\right)\leftrightarrow k\in \left(A\cup B\right)\right)\right)$$
16	6 8 15	pm5.21ndd	$$⊢\phi \to \left(k\in \left(A\mathrm{sadd}B\right)\leftrightarrow k\in \left(A\cup B\right)\right)$$
17	16	eqrdv	$$⊢\phi \to A\mathrm{sadd}B=A\cup B$$