Metamath Proof Explorer

Theorem sadcf

Description: The carry sequence is a sequence of elements of 2o encoding a "sequence of wffs". (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Hypotheses sadval.a 
|- ( ph -> A C_ NN0 )
sadval.b 
|- ( ph -> B C_ NN0 )
sadval.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 ) ) ) )
Assertion sadcf 
|- ( ph -> C : NN0 --> 2o )

Proof

Step Hyp Ref Expression
1 sadval.a 
 |-  ( ph -> A C_ NN0 )
2 sadval.b 
 |-  ( ph -> B C_ NN0 )
3 sadval.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 ) ) ) )
4 0nn0 
 |-  0 e. NN0
5 iftrue 
 |-  ( n = 0 -> if ( n = 0 , (/) , ( n - 1 ) ) = (/) )
6 eqid 
 |-  ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) = ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) )
7 0ex 
 |-  (/) e. _V
8 5 6 7 fvmpt 
 |-  ( 0 e. NN0 -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) = (/) )
9 4 8 ax-mp 
 |-  ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) = (/)
10 7 prid1 
 |-  (/) e. { (/) , 1o }
11 df2o3 
 |-  2o = { (/) , 1o }
12 10 11 eleqtrri 
 |-  (/) e. 2o
13 9 12 eqeltri 
 |-  ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) e. 2o
14 13 a1i 
 |-  ( ph -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) e. 2o )
15 df-ov 
 |-  ( x ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) y ) = ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) ` <. x , y >. )
16 1oex 
 |-  1o e. _V
17 16 prid2 
 |-  1o e. { (/) , 1o }
18 17 11 eleqtrri 
 |-  1o e. 2o
19 18 12 ifcli 
 |-  if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) e. 2o
20 19 rgen2w 
 |-  A. c e. 2o A. m e. NN0 if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) e. 2o
21 eqid 
 |-  ( 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. A , m e. B , (/) e. c ) , 1o , (/) ) )
22 21 fmpo 
 |-  ( A. c e. 2o A. m e. NN0 if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) e. 2o <-> ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) : ( 2o X. NN0 ) --> 2o )
23 20 22 mpbi 
 |-  ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) : ( 2o X. NN0 ) --> 2o
24 23 12 f0cli 
 |-  ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) ` <. x , y >. ) e. 2o
25 15 24 eqeltri 
 |-  ( x ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) y ) e. 2o
26 25 a1i 
 |-  ( ( ph /\ ( x e. 2o /\ y e. _V ) ) -> ( x ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) y ) e. 2o )
27 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
28 0zd 
 |-  ( ph -> 0 e. ZZ )
29 fvexd 
 |-  ( ( ph /\ x e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` x ) e. _V )
30 14 26 27 28 29 seqf2 
 |-  ( ph -> 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 ) ) ) ) : NN0 --> 2o )
31 3 feq1i 
 |-  ( C : NN0 --> 2o <-> 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 ) ) ) ) : NN0 --> 2o )
32 30 31 sylibr 
 |-  ( ph -> C : NN0 --> 2o )