Metamath Proof Explorer

Theorem sadcl

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

Ref Expression
Assertion sadcl ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 0 → A sadd B ⊆ ℕ 0

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 0 → A ⊆ ℕ 0
2 simpr ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 0 → B ⊆ ℕ 0
3 eqid ⊢ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
4 1 2 3 sadfval ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 0 → A sadd B = k ∈ ℕ 0 | hadd k ∈ A k ∈ B ∅ ∈ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k
5 ssrab2 ⊢ k ∈ ℕ 0 | hadd k ∈ A k ∈ B ∅ ∈ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k ⊆ ℕ 0
6 4 5 eqsstrdi ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 0 → A sadd B ⊆ ℕ 0