Theorem sadcom

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

	Ref	Expression
Assertion	sadcom	⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → ( 𝐴 sadd 𝐵 ) = ( 𝐵 sadd 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		hadcoma	⊢ ( hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) ↔ hadd ( 𝑘 ∈ 𝐵 , 𝑘 ∈ 𝐴 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) )
2	1	a1i	⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → ( hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) ↔ hadd ( 𝑘 ∈ 𝐵 , 𝑘 ∈ 𝐴 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) ) )
3	2	rabbidv	⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } = { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐵 , 𝑘 ∈ 𝐴 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } )
4		simpl	⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → 𝐴 ⊆ ℕ0 )
5		simpr	⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → 𝐵 ⊆ ℕ0 )
6		eqid	⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
7	4 5 6	sadfval	⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → ( 𝐴 sadd 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } )
8		cadcoma	⊢ ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) ↔ cadd ( 𝑚 ∈ 𝐵 , 𝑚 ∈ 𝐴 , ∅ ∈ 𝑐 ) )
9	8	a1i	⊢ ( ( 𝑐 ∈ 2o ∧ 𝑚 ∈ ℕ0 ) → ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) ↔ cadd ( 𝑚 ∈ 𝐵 , 𝑚 ∈ 𝐴 , ∅ ∈ 𝑐 ) ) )
10	9	ifbid	⊢ ( ( 𝑐 ∈ 2o ∧ 𝑚 ∈ ℕ0 ) → if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) = if ( cadd ( 𝑚 ∈ 𝐵 , 𝑚 ∈ 𝐴 , ∅ ∈ 𝑐 ) , 1o , ∅ ) )
11	10	mpoeq3ia	⊢ ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) = ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐵 , 𝑚 ∈ 𝐴 , ∅ ∈ 𝑐 ) , 1o , ∅ ) )
12		seqeq2	⊢ ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) = ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐵 , 𝑚 ∈ 𝐴 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) → seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐵 , 𝑚 ∈ 𝐴 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) )
13	11 12	ax-mp	⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐵 , 𝑚 ∈ 𝐴 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
14	5 4 13	sadfval	⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → ( 𝐵 sadd 𝐴 ) = { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐵 , 𝑘 ∈ 𝐴 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } )
15	3 7 14	3eqtr4d	⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → ( 𝐴 sadd 𝐵 ) = ( 𝐵 sadd 𝐴 ) )