Theorem sadcl

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

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

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A C_ NN0 /\ B C_ NN0 ) -> A C_ NN0 )
2		simpr	|- ( ( A C_ NN0 /\ B C_ NN0 ) -> B C_ NN0 )
3		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 ) ) ) )
4	1 2 3	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 ) ) } )
5		ssrab2	|- { 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 ) ) } C_ NN0
6	4 5	eqsstrdi	|- ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A sadd B ) C_ NN0 )