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	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
	saddisj.2	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
	saddisj.3	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
Assertion	saddisj	⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) = ( 𝐴 ∪ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		saddisj.1	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2		saddisj.2	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3		saddisj.3	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
4		sadcl	⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 )
5	1 2 4	syl2anc	⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 )
6	5	sseld	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) → 𝑘 ∈ ℕ0 ) )
7	1 2	unssd	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ ℕ0 )
8	7	sseld	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) → 𝑘 ∈ ℕ0 ) )
9	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ⊆ ℕ0 )
10	2	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ⊆ ℕ0 )
11	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
12		eqid	⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ∅ , ( 𝑥 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ∅ , ( 𝑥 − 1 ) ) ) )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
14	9 10 11 12 13	saddisjlem	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) ↔ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) )
15	14	ex	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) ↔ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) ) )
16	6 8 15	pm5.21ndd	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) ↔ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) )
17	16	eqrdv	⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) = ( 𝐴 ∪ 𝐵 ) )