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→AsaddB=BsaddA

Proof

Step Hyp Ref Expression
1 hadcoma ⊢haddk∈Ak∈B∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k↔haddk∈Bk∈A∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k
2 1 a1i ⊢A⊆ℕ0∧B⊆ℕ0→haddk∈Ak∈B∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k↔haddk∈Bk∈A∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k
3 2 rabbidv ⊢A⊆ℕ0∧B⊆ℕ0→k∈ℕ0|haddk∈Ak∈B∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k=k∈ℕ0|haddk∈Bk∈A∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k
4 simpl ⊢A⊆ℕ0∧B⊆ℕ0→A⊆ℕ0
5 simpr ⊢A⊆ℕ0∧B⊆ℕ0→B⊆ℕ0
6 eqid ⊢seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1
7 4 5 6 sadfval ⊢A⊆ℕ0∧B⊆ℕ0→AsaddB=k∈ℕ0|haddk∈Ak∈B∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k
8 cadcoma ⊢caddm∈Am∈B∅∈c↔caddm∈Bm∈A∅∈c
9 8 a1i ⊢c∈2𝑜∧m∈ℕ0→caddm∈Am∈B∅∈c↔caddm∈Bm∈A∅∈c
10 9 ifbid ⊢c∈2𝑜∧m∈ℕ0→ifcaddm∈Am∈B∅∈c1𝑜∅=ifcaddm∈Bm∈A∅∈c1𝑜∅
11 10 mpoeq3ia ⊢c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅=c∈2𝑜,m∈ℕ0⟼ifcaddm∈Bm∈A∅∈c1𝑜∅
12 seqeq2 ⊢c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅=c∈2𝑜,m∈ℕ0⟼ifcaddm∈Bm∈A∅∈c1𝑜∅→seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Bm∈A∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1
13 11 12 ax-mp ⊢seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Bm∈A∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1
14 5 4 13 sadfval ⊢A⊆ℕ0∧B⊆ℕ0→BsaddA=k∈ℕ0|haddk∈Bk∈A∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k
15 3 7 14 3eqtr4d ⊢A⊆ℕ0∧B⊆ℕ0→AsaddB=BsaddA