Metamath Proof Explorer

Theorem saddisjlem

Description: Lemma for sadadd . (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 ) = (/) )
saddisjlem.c 
|- C = 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 ) ) ) )
saddisjlem.3 
|- ( ph -> N e. NN0 )
Assertion saddisjlem 
|- ( ph -> ( N e. ( A sadd B ) <-> N e. ( 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 saddisjlem.c 
 |-  C = 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 ) ) ) )
5 saddisjlem.3 
 |-  ( ph -> N e. NN0 )
6 1 2 4 5 sadval 
 |-  ( ph -> ( N e. ( A sadd B ) <-> hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
7 fveq2 
 |-  ( x = 0 -> ( C ` x ) = ( C ` 0 ) )
8 7 eleq2d 
 |-  ( x = 0 -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` 0 ) ) )
9 8 notbid 
 |-  ( x = 0 -> ( -. (/) e. ( C ` x ) <-> -. (/) e. ( C ` 0 ) ) )
10 9 imbi2d 
 |-  ( x = 0 -> ( ( ph -> -. (/) e. ( C ` x ) ) <-> ( ph -> -. (/) e. ( C ` 0 ) ) ) )
11 fveq2 
 |-  ( x = k -> ( C ` x ) = ( C ` k ) )
12 11 eleq2d 
 |-  ( x = k -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` k ) ) )
13 12 notbid 
 |-  ( x = k -> ( -. (/) e. ( C ` x ) <-> -. (/) e. ( C ` k ) ) )
14 13 imbi2d 
 |-  ( x = k -> ( ( ph -> -. (/) e. ( C ` x ) ) <-> ( ph -> -. (/) e. ( C ` k ) ) ) )
15 fveq2 
 |-  ( x = ( k + 1 ) -> ( C ` x ) = ( C ` ( k + 1 ) ) )
16 15 eleq2d 
 |-  ( x = ( k + 1 ) -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` ( k + 1 ) ) ) )
17 16 notbid 
 |-  ( x = ( k + 1 ) -> ( -. (/) e. ( C ` x ) <-> -. (/) e. ( C ` ( k + 1 ) ) ) )
18 17 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ph -> -. (/) e. ( C ` x ) ) <-> ( ph -> -. (/) e. ( C ` ( k + 1 ) ) ) ) )
19 fveq2 
 |-  ( x = N -> ( C ` x ) = ( C ` N ) )
20 19 eleq2d 
 |-  ( x = N -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` N ) ) )
21 20 notbid 
 |-  ( x = N -> ( -. (/) e. ( C ` x ) <-> -. (/) e. ( C ` N ) ) )
22 21 imbi2d 
 |-  ( x = N -> ( ( ph -> -. (/) e. ( C ` x ) ) <-> ( ph -> -. (/) e. ( C ` N ) ) ) )
23 1 2 4 sadc0 
 |-  ( ph -> -. (/) e. ( C ` 0 ) )
24 noel 
 |-  -. k e. (/)
25 1 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. (/) e. ( C ` k ) ) -> A C_ NN0 )
26 2 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. (/) e. ( C ` k ) ) -> B C_ NN0 )
27 simplr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. (/) e. ( C ` k ) ) -> k e. NN0 )
28 25 26 4 27 sadcp1 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. (/) e. ( C ` k ) ) -> ( (/) e. ( C ` ( k + 1 ) ) <-> cadd ( k e. A , k e. B , (/) e. ( C ` k ) ) ) )
29 cad0 
 |-  ( -. (/) e. ( C ` k ) -> ( cadd ( k e. A , k e. B , (/) e. ( C ` k ) ) <-> ( k e. A /\ k e. B ) ) )
30 29 adantl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. (/) e. ( C ` k ) ) -> ( cadd ( k e. A , k e. B , (/) e. ( C ` k ) ) <-> ( k e. A /\ k e. B ) ) )
31 elin 
 |-  ( k e. ( A i^i B ) <-> ( k e. A /\ k e. B ) )
32 3 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. (/) e. ( C ` k ) ) -> ( A i^i B ) = (/) )
33 32 eleq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. (/) e. ( C ` k ) ) -> ( k e. ( A i^i B ) <-> k e. (/) ) )
34 31 33 bitr3id 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. (/) e. ( C ` k ) ) -> ( ( k e. A /\ k e. B ) <-> k e. (/) ) )
35 28 30 34 3bitrd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. (/) e. ( C ` k ) ) -> ( (/) e. ( C ` ( k + 1 ) ) <-> k e. (/) ) )
36 24 35 mtbiri 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. (/) e. ( C ` k ) ) -> -. (/) e. ( C ` ( k + 1 ) ) )
37 36 ex 
 |-  ( ( ph /\ k e. NN0 ) -> ( -. (/) e. ( C ` k ) -> -. (/) e. ( C ` ( k + 1 ) ) ) )
38 37 expcom 
 |-  ( k e. NN0 -> ( ph -> ( -. (/) e. ( C ` k ) -> -. (/) e. ( C ` ( k + 1 ) ) ) ) )
39 38 a2d 
 |-  ( k e. NN0 -> ( ( ph -> -. (/) e. ( C ` k ) ) -> ( ph -> -. (/) e. ( C ` ( k + 1 ) ) ) ) )
40 10 14 18 22 23 39 nn0ind 
 |-  ( N e. NN0 -> ( ph -> -. (/) e. ( C ` N ) ) )
41 5 40 mpcom 
 |-  ( ph -> -. (/) e. ( C ` N ) )
42 hadrot 
 |-  ( hadd ( (/) e. ( C ` N ) , N e. A , N e. B ) <-> hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) )
43 had0 
 |-  ( -. (/) e. ( C ` N ) -> ( hadd ( (/) e. ( C ` N ) , N e. A , N e. B ) <-> ( N e. A \/_ N e. B ) ) )
44 42 43 bitr3id 
 |-  ( -. (/) e. ( C ` N ) -> ( hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( N e. A \/_ N e. B ) ) )
45 41 44 syl 
 |-  ( ph -> ( hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( N e. A \/_ N e. B ) ) )
46 noel 
 |-  -. N e. (/)
47 elin 
 |-  ( N e. ( A i^i B ) <-> ( N e. A /\ N e. B ) )
48 3 eleq2d 
 |-  ( ph -> ( N e. ( A i^i B ) <-> N e. (/) ) )
49 47 48 bitr3id 
 |-  ( ph -> ( ( N e. A /\ N e. B ) <-> N e. (/) ) )
50 46 49 mtbiri 
 |-  ( ph -> -. ( N e. A /\ N e. B ) )
51 xor2 
 |-  ( ( N e. A \/_ N e. B ) <-> ( ( N e. A \/ N e. B ) /\ -. ( N e. A /\ N e. B ) ) )
52 51 rbaib 
 |-  ( -. ( N e. A /\ N e. B ) -> ( ( N e. A \/_ N e. B ) <-> ( N e. A \/ N e. B ) ) )
53 50 52 syl 
 |-  ( ph -> ( ( N e. A \/_ N e. B ) <-> ( N e. A \/ N e. B ) ) )
54 elun 
 |-  ( N e. ( A u. B ) <-> ( N e. A \/ N e. B ) )
55 53 54 bitr4di 
 |-  ( ph -> ( ( N e. A \/_ N e. B ) <-> N e. ( A u. B ) ) )
56 6 45 55 3bitrd 
 |-  ( ph -> ( N e. ( A sadd B ) <-> N e. ( A u. B ) ) )