Metamath Proof Explorer

Theorem sadcom

Description: The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016)

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

Proof

Step Hyp Ref Expression
1 hadcoma ⊢ 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 ↔ hadd k ∈ B k ∈ A ∅ ∈ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k
2 1 a1i ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 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 ↔ hadd k ∈ B k ∈ A ∅ ∈ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k
3 2 rabbidv ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 0 → 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 = k ∈ ℕ 0 | hadd k ∈ B k ∈ A ∅ ∈ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k
4 simpl ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 0 → A ⊆ ℕ 0
5 simpr ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 0 → B ⊆ ℕ 0
6 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
7 4 5 6 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
8 cadcoma ⊢ cadd m ∈ A m ∈ B ∅ ∈ c ↔ cadd m ∈ B m ∈ A ∅ ∈ c
9 8 a1i ⊢ c ∈ 2 𝑜 ∧ m ∈ ℕ 0 → cadd m ∈ A m ∈ B ∅ ∈ c ↔ cadd m ∈ B m ∈ A ∅ ∈ c
10 9 ifbid ⊢ c ∈ 2 𝑜 ∧ m ∈ ℕ 0 → if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ = if cadd m ∈ B m ∈ A ∅ ∈ c 1 𝑜 ∅
11 10 mpoeq3ia ⊢ c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ = c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ B m ∈ A ∅ ∈ c 1 𝑜 ∅
12 seqeq2 ⊢ c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ = c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ B m ∈ A ∅ ∈ c 1 𝑜 ∅ → 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 ∈ B m ∈ A ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
13 11 12 ax-mp ⊢ 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 ∈ B m ∈ A ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
14 5 4 13 sadfval ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 0 → B sadd A = k ∈ ℕ 0 | hadd k ∈ B k ∈ A ∅ ∈ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k
15 3 7 14 3eqtr4d ⊢ A ⊆ ℕ 0 ∧ B ⊆ ℕ 0 → A sadd B = B sadd A