Theorem saddisj

Description: The sum of disjoint sequences is the union of the sequences. (In this case, there are no carried bits.) (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	saddisj.1	|- ( ph -> A C_ NN0 )
	saddisj.2	|- ( ph -> B C_ NN0 )
	saddisj.3	|- ( ph -> ( A i^i B ) = (/) )
Assertion	saddisj	|- ( ph -> ( A sadd B ) = ( A u. B ) )

Proof

Step	Hyp	Ref	Expression
1		saddisj.1	|- ( ph -> A C_ NN0 )
2		saddisj.2	|- ( ph -> B C_ NN0 )
3		saddisj.3	|- ( ph -> ( A i^i B ) = (/) )
4		sadcl	|- ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A sadd B ) C_ NN0 )
5	1 2 4	syl2anc	|- ( ph -> ( A sadd B ) C_ NN0 )
6	5	sseld	|- ( ph -> ( k e. ( A sadd B ) -> k e. NN0 ) )
7	1 2	unssd	|- ( ph -> ( A u. B ) C_ NN0 )
8	7	sseld	|- ( ph -> ( k e. ( A u. B ) -> k e. NN0 ) )
9	1	adantr	|- ( ( ph /\ k e. NN0 ) -> A C_ NN0 )
10	2	adantr	|- ( ( ph /\ k e. NN0 ) -> B C_ NN0 )
11	3	adantr	|- ( ( ph /\ k e. NN0 ) -> ( A i^i B ) = (/) )
12		eqid	|- seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( x e. NN0 |-> if ( x = 0 , (/) , ( x - 1 ) ) ) ) = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( x e. NN0 |-> if ( x = 0 , (/) , ( x - 1 ) ) ) )
13		simpr	|- ( ( ph /\ k e. NN0 ) -> k e. NN0 )
14	9 10 11 12 13	saddisjlem	|- ( ( ph /\ k e. NN0 ) -> ( k e. ( A sadd B ) <-> k e. ( A u. B ) ) )
15	14	ex	|- ( ph -> ( k e. NN0 -> ( k e. ( A sadd B ) <-> k e. ( A u. B ) ) ) )
16	6 8 15	pm5.21ndd	|- ( ph -> ( k e. ( A sadd B ) <-> k e. ( A u. B ) ) )
17	16	eqrdv	|- ( ph -> ( A sadd B ) = ( A u. B ) )