Metamath Proof Explorer

Theorem sadcom

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

		Ref	Expression
	Assertion	sadcom	\|- ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A sadd B ) = ( B sadd A ) )

Proof

Step	Hyp	Ref	Expression
1		hadcoma	\|- ( hadd ( k e. A , k e. B , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) <-> hadd ( k e. B , k e. A , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) )
2	1	a1i	\|- ( ( A C_ NN0 /\ B C_ NN0 ) -> ( hadd ( k e. A , k e. B , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) <-> hadd ( k e. B , k e. A , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) ) )
3	2	rabbidv	\|- ( ( A C_ NN0 /\ B C_ NN0 ) -> { k e. NN0 \| hadd ( k e. A , k e. B , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) } = { k e. NN0 \| hadd ( k e. B , k e. A , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) } )
4		simpl	\|- ( ( A C_ NN0 /\ B C_ NN0 ) -> A C_ NN0 )
5		simpr	\|- ( ( A C_ NN0 /\ B C_ NN0 ) -> B C_ NN0 )
6		eqid	\|- seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
7	4 5 6	sadfval	\|- ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A sadd B ) = { k e. NN0 \| hadd ( k e. A , k e. B , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) } )
8		cadcoma	\|- ( cadd ( m e. A , m e. B , (/) e. c ) <-> cadd ( m e. B , m e. A , (/) e. c ) )
9	8	a1i	\|- ( ( c e. 2o /\ m e. NN0 ) -> ( cadd ( m e. A , m e. B , (/) e. c ) <-> cadd ( m e. B , m e. A , (/) e. c ) ) )
10	9	ifbid	\|- ( ( c e. 2o /\ m e. NN0 ) -> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) = if ( cadd ( m e. B , m e. A , (/) e. c ) , 1o , (/) ) )
11	10	mpoeq3ia	\|- ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) = ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. B , m e. A , (/) e. c ) , 1o , (/) ) )
12		seqeq2	\|- ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) = ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. B , m e. A , (/) e. c ) , 1o , (/) ) ) -> seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. B , m e. A , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) )
13	11 12	ax-mp	\|- seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. B , m e. A , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
14	5 4 13	sadfval	\|- ( ( A C_ NN0 /\ B C_ NN0 ) -> ( B sadd A ) = { k e. NN0 \| hadd ( k e. B , k e. A , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 \|-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 \|-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) } )
15	3 7 14	3eqtr4d	\|- ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A sadd B ) = ( B sadd A ) )