Metamath Proof Explorer

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 ⊢ φ → A ⊆ ℕ 0
saddisj.2 ⊢ φ → B ⊆ ℕ 0
saddisj.3 ⊢ φ → A ∩ B = ∅
Assertion saddisj ⊢ φ → A sadd B = A ∪ B

Proof

Step Hyp Ref Expression
1 saddisj.1 ⊢ φ → A ⊆ ℕ 0
2 saddisj.2 ⊢ φ → B ⊆ ℕ 0
3 saddisj.3 ⊢ φ → A ∩ B = ∅
4 sadcl ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 0 → A sadd B ⊆ ℕ 0
5 1 2 4 syl2anc ⊢ φ → A sadd B ⊆ ℕ 0
6 5 sseld ⊢ φ → k ∈ A sadd B → k ∈ ℕ 0
7 1 2 unssd ⊢ φ → A ∪ B ⊆ ℕ 0
8 7 sseld ⊢ φ → k ∈ A ∪ B → k ∈ ℕ 0
9 1 adantr ⊢ φ ∧ k ∈ ℕ 0 → A ⊆ ℕ 0
10 2 adantr ⊢ φ ∧ k ∈ ℕ 0 → B ⊆ ℕ 0
11 3 adantr ⊢ φ ∧ k ∈ ℕ 0 → A ∩ B = ∅
12 eqid ⊢ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ x ∈ ℕ 0 ⟼ if x = 0 ∅ x − 1 = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ x ∈ ℕ 0 ⟼ if x = 0 ∅ x − 1
13 simpr ⊢ φ ∧ k ∈ ℕ 0 → k ∈ ℕ 0
14 9 10 11 12 13 saddisjlem ⊢ φ ∧ k ∈ ℕ 0 → k ∈ A sadd B ↔ k ∈ A ∪ B
15 14 ex ⊢ φ → k ∈ ℕ 0 → k ∈ A sadd B ↔ k ∈ A ∪ B
16 6 8 15 pm5.21ndd ⊢ φ → k ∈ A sadd B ↔ k ∈ A ∪ B
17 16 eqrdv ⊢ φ → A sadd B = A ∪ B