ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ennnfonelemkh Unicode version

Theorem ennnfonelemkh 12426
Description: Lemma for ennnfone 12439. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.)
Hypotheses
Ref Expression
ennnfonelemh.dceq  |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )
ennnfonelemh.f  |-  ( ph  ->  F : om -onto-> A
)
ennnfonelemh.ne  |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j ) )
ennnfonelemh.g  |-  G  =  ( x  e.  ( A  ^pm  om ) ,  y  e.  om  |->  if ( ( F `  y )  e.  ( F " y ) ,  x ,  ( x  u.  { <. dom  x ,  ( F `
 y ) >. } ) ) )
ennnfonelemh.n  |-  N  = frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )
ennnfonelemh.j  |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/) ,  ( `' N `  ( x  -  1 ) ) ) )
ennnfonelemh.h  |-  H  =  seq 0 ( G ,  J )
ennnfonelemkh.p  |-  ( ph  ->  P  e.  NN0 )
Assertion
Ref Expression
ennnfonelemkh  |-  ( ph  ->  dom  ( H `  P )  C_  ( `' N `  P ) )
Distinct variable groups:    A, j, x, y    x, F, y   
j, G    j, H, x, y    j, J    j, N, x, y    ph, j, x, y
Allowed substitution hints:    ph( k, n)    A( k, n)    P( x, y, j, k, n)    F( j, k, n)    G( x, y, k, n)    H( k, n)    J( x, y, k, n)    N( k, n)

Proof of Theorem ennnfonelemkh
Dummy variables  m  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ennnfonelemkh.p . 2  |-  ( ph  ->  P  e.  NN0 )
2 fveq2 5527 . . . . . . 7  |-  ( w  =  0  ->  ( H `  w )  =  ( H ` 
0 ) )
32dmeqd 4841 . . . . . 6  |-  ( w  =  0  ->  dom  ( H `  w )  =  dom  ( H `
 0 ) )
4 fveq2 5527 . . . . . 6  |-  ( w  =  0  ->  ( `' N `  w )  =  ( `' N `  0 ) )
53, 4sseq12d 3198 . . . . 5  |-  ( w  =  0  ->  ( dom  ( H `  w
)  C_  ( `' N `  w )  <->  dom  ( H `  0
)  C_  ( `' N `  0 )
) )
65imbi2d 230 . . . 4  |-  ( w  =  0  ->  (
( ph  ->  dom  ( H `  w )  C_  ( `' N `  w ) )  <->  ( ph  ->  dom  ( H ` 
0 )  C_  ( `' N `  0 ) ) ) )
7 fveq2 5527 . . . . . . 7  |-  ( w  =  m  ->  ( H `  w )  =  ( H `  m ) )
87dmeqd 4841 . . . . . 6  |-  ( w  =  m  ->  dom  ( H `  w )  =  dom  ( H `
 m ) )
9 fveq2 5527 . . . . . 6  |-  ( w  =  m  ->  ( `' N `  w )  =  ( `' N `  m ) )
108, 9sseq12d 3198 . . . . 5  |-  ( w  =  m  ->  ( dom  ( H `  w
)  C_  ( `' N `  w )  <->  dom  ( H `  m
)  C_  ( `' N `  m )
) )
1110imbi2d 230 . . . 4  |-  ( w  =  m  ->  (
( ph  ->  dom  ( H `  w )  C_  ( `' N `  w ) )  <->  ( ph  ->  dom  ( H `  m )  C_  ( `' N `  m ) ) ) )
12 fveq2 5527 . . . . . . 7  |-  ( w  =  ( m  + 
1 )  ->  ( H `  w )  =  ( H `  ( m  +  1
) ) )
1312dmeqd 4841 . . . . . 6  |-  ( w  =  ( m  + 
1 )  ->  dom  ( H `  w )  =  dom  ( H `
 ( m  + 
1 ) ) )
14 fveq2 5527 . . . . . 6  |-  ( w  =  ( m  + 
1 )  ->  ( `' N `  w )  =  ( `' N `  ( m  +  1 ) ) )
1513, 14sseq12d 3198 . . . . 5  |-  ( w  =  ( m  + 
1 )  ->  ( dom  ( H `  w
)  C_  ( `' N `  w )  <->  dom  ( H `  (
m  +  1 ) )  C_  ( `' N `  ( m  +  1 ) ) ) )
1615imbi2d 230 . . . 4  |-  ( w  =  ( m  + 
1 )  ->  (
( ph  ->  dom  ( H `  w )  C_  ( `' N `  w ) )  <->  ( ph  ->  dom  ( H `  ( m  +  1
) )  C_  ( `' N `  ( m  +  1 ) ) ) ) )
17 fveq2 5527 . . . . . . 7  |-  ( w  =  P  ->  ( H `  w )  =  ( H `  P ) )
1817dmeqd 4841 . . . . . 6  |-  ( w  =  P  ->  dom  ( H `  w )  =  dom  ( H `
 P ) )
19 fveq2 5527 . . . . . 6  |-  ( w  =  P  ->  ( `' N `  w )  =  ( `' N `  P ) )
2018, 19sseq12d 3198 . . . . 5  |-  ( w  =  P  ->  ( dom  ( H `  w
)  C_  ( `' N `  w )  <->  dom  ( H `  P
)  C_  ( `' N `  P )
) )
2120imbi2d 230 . . . 4  |-  ( w  =  P  ->  (
( ph  ->  dom  ( H `  w )  C_  ( `' N `  w ) )  <->  ( ph  ->  dom  ( H `  P )  C_  ( `' N `  P ) ) ) )
22 ennnfonelemh.dceq . . . . . . . . 9  |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )
23 ennnfonelemh.f . . . . . . . . 9  |-  ( ph  ->  F : om -onto-> A
)
24 ennnfonelemh.ne . . . . . . . . 9  |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j ) )
25 ennnfonelemh.g . . . . . . . . 9  |-  G  =  ( x  e.  ( A  ^pm  om ) ,  y  e.  om  |->  if ( ( F `  y )  e.  ( F " y ) ,  x ,  ( x  u.  { <. dom  x ,  ( F `
 y ) >. } ) ) )
26 ennnfonelemh.n . . . . . . . . 9  |-  N  = frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )
27 ennnfonelemh.j . . . . . . . . 9  |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/) ,  ( `' N `  ( x  -  1 ) ) ) )
28 ennnfonelemh.h . . . . . . . . 9  |-  H  =  seq 0 ( G ,  J )
2922, 23, 24, 25, 26, 27, 28ennnfonelem0 12419 . . . . . . . 8  |-  ( ph  ->  ( H `  0
)  =  (/) )
3029dmeqd 4841 . . . . . . 7  |-  ( ph  ->  dom  ( H ` 
0 )  =  dom  (/) )
31 dm0 4853 . . . . . . 7  |-  dom  (/)  =  (/)
3230, 31eqtrdi 2236 . . . . . 6  |-  ( ph  ->  dom  ( H ` 
0 )  =  (/) )
33 0ss 3473 . . . . . 6  |-  (/)  C_  ( `' N `  0 )
3432, 33eqsstrdi 3219 . . . . 5  |-  ( ph  ->  dom  ( H ` 
0 )  C_  ( `' N `  0 ) )
3534a1i 9 . . . 4  |-  ( 0  e.  ZZ  ->  ( ph  ->  dom  ( H `  0 )  C_  ( `' N `  0 ) ) )
3626frechashgf1o 10441 . . . . . . . . . . . . . 14  |-  N : om
-1-1-onto-> NN0
37 f1of 5473 . . . . . . . . . . . . . 14  |-  ( N : om -1-1-onto-> NN0  ->  N : om
--> NN0 )
3836, 37mp1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  N : om --> NN0 )
3922ad2antrr 488 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y
)
4023ad2antrr 488 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  F : om -onto-> A )
4124ad2antrr 488 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  A. n  e.  om  E. k  e. 
om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )
)
42 simplr 528 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  m  e.  ( ZZ>= `  0 )
)
43 nn0uz 9575 . . . . . . . . . . . . . . . . 17  |-  NN0  =  ( ZZ>= `  0 )
4442, 43eleqtrrdi 2281 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  m  e.  NN0 )
45 peano2nn0 9229 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN0  ->  ( m  +  1 )  e. 
NN0 )
4644, 45syl 14 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( m  +  1 )  e. 
NN0 )
4739, 40, 41, 25, 26, 27, 28, 46ennnfonelemom 12422 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  dom  ( H `
 ( m  + 
1 ) )  e. 
om )
4847adantr 276 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  dom  ( H `  ( m  +  1 ) )  e.  om )
4938, 48ffvelcdmd 5665 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( N `  dom  ( H `
 ( m  + 
1 ) ) )  e.  NN0 )
5049nn0red 9243 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( N `  dom  ( H `
 ( m  + 
1 ) ) )  e.  RR )
5144nn0red 9243 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  m  e.  RR )
5251adantr 276 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  m  e.  RR )
53 peano2re 8106 . . . . . . . . . . . 12  |-  ( m  e.  RR  ->  (
m  +  1 )  e.  RR )
5452, 53syl 14 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  (
m  +  1 )  e.  RR )
5539, 40, 41, 25, 26, 27, 28, 44ennnfonelemp1 12420 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( H `  ( m  +  1 ) )  =  if ( ( F `  ( `' N `  m ) )  e.  ( F
" ( `' N `  m ) ) ,  ( H `  m
) ,  ( ( H `  m )  u.  { <. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. } ) ) )
5655adantr 276 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( H `  ( m  +  1 ) )  =  if ( ( F `  ( `' N `  m ) )  e.  ( F
" ( `' N `  m ) ) ,  ( H `  m
) ,  ( ( H `  m )  u.  { <. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. } ) ) )
57 simpr 110 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )
5857iftrued 3553 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  if ( ( F `  ( `' N `  m ) )  e.  ( F
" ( `' N `  m ) ) ,  ( H `  m
) ,  ( ( H `  m )  u.  { <. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. } ) )  =  ( H `  m ) )
5956, 58eqtrd 2220 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( H `  ( m  +  1 ) )  =  ( H `  m ) )
6059dmeqd 4841 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  dom  ( H `  ( m  +  1 ) )  =  dom  ( H `
 m ) )
6160fveq2d 5531 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( N `  dom  ( H `
 ( m  + 
1 ) ) )  =  ( N `  dom  ( H `  m
) ) )
62 simpr 110 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  dom  ( H `
 m )  C_  ( `' N `  m ) )
63 0zd 9278 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  0  e.  ZZ )
6439, 40, 41, 25, 26, 27, 28, 44ennnfonelemom 12422 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  dom  ( H `
 m )  e. 
om )
65 f1ocnv 5486 . . . . . . . . . . . . . . . . . . . 20  |-  ( N : om -1-1-onto-> NN0  ->  `' N : NN0
-1-1-onto-> om )
6636, 65ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  `' N : NN0
-1-1-onto-> om
67 f1of 5473 . . . . . . . . . . . . . . . . . . 19  |-  ( `' N : NN0 -1-1-onto-> om  ->  `' N : NN0 --> om )
6866, 67mp1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  NN0  ->  `' N : NN0 --> om )
69 id 19 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  NN0  ->  m  e. 
NN0 )
7068, 69ffvelcdmd 5665 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  NN0  ->  ( `' N `  m )  e.  om )
7144, 70syl 14 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( `' N `  m )  e.  om )
7263, 26, 64, 71frec2uzled 10442 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( dom  ( H `  m ) 
C_  ( `' N `  m )  <->  ( N `  dom  ( H `  m ) )  <_ 
( N `  ( `' N `  m ) ) ) )
7362, 72mpbid 147 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( N `  dom  ( H `  m ) )  <_ 
( N `  ( `' N `  m ) ) )
74 f1ocnvfv2 5792 . . . . . . . . . . . . . . 15  |-  ( ( N : om -1-1-onto-> NN0  /\  m  e. 
NN0 )  ->  ( N `  ( `' N `  m )
)  =  m )
7536, 44, 74sylancr 414 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( N `  ( `' N `  m ) )  =  m )
7673, 75breqtrd 4041 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( N `  dom  ( H `  m ) )  <_  m )
7776adantr 276 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( N `  dom  ( H `
 m ) )  <_  m )
7861, 77eqbrtrd 4037 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( N `  dom  ( H `
 ( m  + 
1 ) ) )  <_  m )
7952lep1d 8901 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  m  <_  ( m  +  1 ) )
8050, 52, 54, 78, 79letrd 8094 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( N `  dom  ( H `
 ( m  + 
1 ) ) )  <_  ( m  + 
1 ) )
81 f1ocnvfv2 5792 . . . . . . . . . . . 12  |-  ( ( N : om -1-1-onto-> NN0  /\  ( m  +  1 )  e. 
NN0 )  ->  ( N `  ( `' N `  ( m  +  1 ) ) )  =  ( m  +  1 ) )
8236, 46, 81sylancr 414 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( N `  ( `' N `  ( m  +  1
) ) )  =  ( m  +  1 ) )
8382adantr 276 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( N `  ( `' N `  ( m  +  1 ) ) )  =  ( m  +  1 ) )
8480, 83breqtrrd 4043 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( N `  dom  ( H `
 ( m  + 
1 ) ) )  <_  ( N `  ( `' N `  ( m  +  1 ) ) ) )
8566, 67mp1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  `' N : NN0 --> om )
8685, 46ffvelcdmd 5665 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( `' N `  ( m  +  1 ) )  e.  om )
8763, 26, 47, 86frec2uzled 10442 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( dom  ( H `  ( m  +  1 ) ) 
C_  ( `' N `  ( m  +  1 ) )  <->  ( N `  dom  ( H `  ( m  +  1
) ) )  <_ 
( N `  ( `' N `  ( m  +  1 ) ) ) ) )
8887adantr 276 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  ( dom  ( H `  (
m  +  1 ) )  C_  ( `' N `  ( m  +  1 ) )  <-> 
( N `  dom  ( H `  ( m  +  1 ) ) )  <_  ( N `  ( `' N `  ( m  +  1
) ) ) ) )
8984, 88mpbird 167 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  dom  ( H `  ( m  +  1 ) ) 
C_  ( `' N `  ( m  +  1 ) ) )
9055adantr 276 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( H `  ( m  +  1
) )  =  if ( ( F `  ( `' N `  m ) )  e.  ( F
" ( `' N `  m ) ) ,  ( H `  m
) ,  ( ( H `  m )  u.  { <. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. } ) ) )
91 simpr 110 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  -.  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )
9291iffalsed 3556 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  if ( ( F `  ( `' N `  m ) )  e.  ( F
" ( `' N `  m ) ) ,  ( H `  m
) ,  ( ( H `  m )  u.  { <. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. } ) )  =  ( ( H `
 m )  u. 
{ <. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. } ) )
9390, 92eqtrd 2220 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( H `  ( m  +  1
) )  =  ( ( H `  m
)  u.  { <. dom  ( H `  m
) ,  ( F `
 ( `' N `  m ) ) >. } ) )
9493dmeqd 4841 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  dom  ( H `  ( m  +  1 ) )  =  dom  ( ( H `  m )  u.  { <. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. } ) )
95 dmun 4846 . . . . . . . . . . . . . . . 16  |-  dom  (
( H `  m
)  u.  { <. dom  ( H `  m
) ,  ( F `
 ( `' N `  m ) ) >. } )  =  ( dom  ( H `  m )  u.  dom  {
<. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. } )
9694, 95eqtrdi 2236 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  dom  ( H `  ( m  +  1 ) )  =  ( dom  ( H `  m )  u.  dom  {
<. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. } ) )
97 fof 5450 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : om -onto-> A  ->  F : om --> A )
9840, 97syl 14 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  F : om
--> A )
9998, 71ffvelcdmd 5665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( F `  ( `' N `  m ) )  e.  A )
10099adantr 276 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( F `  ( `' N `  m ) )  e.  A )
101 dmsnopg 5112 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  ( `' N `  m ) )  e.  A  ->  dom  { <. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. }  =  { dom  ( H `  m
) } )
102100, 101syl 14 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  dom  { <. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. }  =  { dom  ( H `  m
) } )
103102uneq2d 3301 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( dom  ( H `  m )  u.  dom  { <. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. } )  =  ( dom  ( H `
 m )  u. 
{ dom  ( H `  m ) } ) )
10496, 103eqtrd 2220 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  dom  ( H `  ( m  +  1 ) )  =  ( dom  ( H `  m )  u.  { dom  ( H `  m
) } ) )
105 df-suc 4383 . . . . . . . . . . . . . 14  |-  suc  dom  ( H `  m )  =  ( dom  ( H `  m )  u.  { dom  ( H `
 m ) } )
106104, 105eqtr4di 2238 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  dom  ( H `  ( m  +  1 ) )  =  suc  dom  ( H `  m
) )
107 simplr 528 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  dom  ( H `  m )  C_  ( `' N `  m ) )
10871adantr 276 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( `' N `  m )  e.  om )
109 nnsucsssuc 6506 . . . . . . . . . . . . . . 15  |-  ( ( dom  ( H `  m )  e.  om  /\  ( `' N `  m )  e.  om )  ->  ( dom  ( H `  m )  C_  ( `' N `  m )  <->  suc  dom  ( H `  m )  C_ 
suc  ( `' N `  m ) ) )
11064, 108, 109syl2an2r 595 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( dom  ( H `  m )  C_  ( `' N `  m )  <->  suc  dom  ( H `  m )  C_ 
suc  ( `' N `  m ) ) )
111107, 110mpbid 147 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  suc  dom  ( H `
 m )  C_  suc  ( `' N `  m ) )
112106, 111eqsstrd 3203 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  dom  ( H `  ( m  +  1 ) )  C_  suc  ( `' N `  m ) )
113 0zd 9278 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  0  e.  ZZ )
11447adantr 276 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  dom  ( H `  ( m  +  1 ) )  e.  om )
115 peano2 4606 . . . . . . . . . . . . . 14  |-  ( ( `' N `  m )  e.  om  ->  suc  ( `' N `  m )  e.  om )
116108, 115syl 14 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  suc  ( `' N `  m )  e.  om )
117113, 26, 114, 116frec2uzled 10442 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( dom  ( H `  ( m  +  1 ) ) 
C_  suc  ( `' N `  m )  <->  ( N `  dom  ( H `  ( m  +  1 ) ) )  <_  ( N `  suc  ( `' N `  m ) ) ) )
118112, 117mpbid 147 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( N `  dom  ( H `  (
m  +  1 ) ) )  <_  ( N `  suc  ( `' N `  m ) ) )
119113, 26, 108frec2uzsucd 10414 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( N `  suc  ( `' N `  m ) )  =  ( ( N `  ( `' N `  m ) )  +  1 ) )
12075adantr 276 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( N `  ( `' N `  m ) )  =  m )
121120oveq1d 5903 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( ( N `
 ( `' N `  m ) )  +  1 )  =  ( m  +  1 ) )
122119, 121eqtrd 2220 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( N `  suc  ( `' N `  m ) )  =  ( m  +  1 ) )
123118, 122breqtrd 4041 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( N `  dom  ( H `  (
m  +  1 ) ) )  <_  (
m  +  1 ) )
12482adantr 276 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( N `  ( `' N `  ( m  +  1 ) ) )  =  ( m  +  1 ) )
125123, 124breqtrrd 4043 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( N `  dom  ( H `  (
m  +  1 ) ) )  <_  ( N `  ( `' N `  ( m  +  1 ) ) ) )
12686adantr 276 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( `' N `  ( m  +  1 ) )  e.  om )
127113, 26, 114, 126frec2uzled 10442 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( dom  ( H `  ( m  +  1 ) ) 
C_  ( `' N `  ( m  +  1 ) )  <->  ( N `  dom  ( H `  ( m  +  1
) ) )  <_ 
( N `  ( `' N `  ( m  +  1 ) ) ) ) )
128125, 127mpbird 167 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  dom  ( H `  ( m  +  1 ) )  C_  ( `' N `  ( m  +  1 ) ) )
12939, 40, 71ennnfonelemdc 12413 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  -> DECID  ( F `  ( `' N `  m ) )  e.  ( F
" ( `' N `  m ) ) )
130 exmiddc 837 . . . . . . . . 9  |-  (DECID  ( F `
 ( `' N `  m ) )  e.  ( F " ( `' N `  m ) )  ->  ( ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) )  \/ 
-.  ( F `  ( `' N `  m ) )  e.  ( F
" ( `' N `  m ) ) ) )
131129, 130syl 14 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) )  \/ 
-.  ( F `  ( `' N `  m ) )  e.  ( F
" ( `' N `  m ) ) ) )
13289, 128, 131mpjaodan 799 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  dom  ( H `
 ( m  + 
1 ) )  C_  ( `' N `  ( m  +  1 ) ) )
133132ex 115 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  0 )
)  ->  ( dom  ( H `  m ) 
C_  ( `' N `  m )  ->  dom  ( H `  ( m  +  1 ) ) 
C_  ( `' N `  ( m  +  1 ) ) ) )
134133expcom 116 . . . . 5  |-  ( m  e.  ( ZZ>= `  0
)  ->  ( ph  ->  ( dom  ( H `
 m )  C_  ( `' N `  m )  ->  dom  ( H `  ( m  +  1 ) )  C_  ( `' N `  ( m  +  1 ) ) ) ) )
135134a2d 26 . . . 4  |-  ( m  e.  ( ZZ>= `  0
)  ->  ( ( ph  ->  dom  ( H `  m )  C_  ( `' N `  m ) )  ->  ( ph  ->  dom  ( H `  ( m  +  1
) )  C_  ( `' N `  ( m  +  1 ) ) ) ) )
1366, 11, 16, 21, 35, 135uzind4 9601 . . 3  |-  ( P  e.  ( ZZ>= `  0
)  ->  ( ph  ->  dom  ( H `  P )  C_  ( `' N `  P ) ) )
137136, 43eleq2s 2282 . 2  |-  ( P  e.  NN0  ->  ( ph  ->  dom  ( H `  P )  C_  ( `' N `  P ) ) )
1381, 137mpcom 36 1  |-  ( ph  ->  dom  ( H `  P )  C_  ( `' N `  P ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 709  DECID wdc 835    = wceq 1363    e. wcel 2158    =/= wne 2357   A.wral 2465   E.wrex 2466    u. cun 3139    C_ wss 3141   (/)c0 3434   ifcif 3546   {csn 3604   <.cop 3607   class class class wbr 4015    |-> cmpt 4076   suc csuc 4377   omcom 4601   `'ccnv 4637   dom cdm 4638   "cima 4641   -->wf 5224   -onto->wfo 5226   -1-1-onto->wf1o 5227   ` cfv 5228  (class class class)co 5888    e. cmpo 5890  freccfrec 6404    ^pm cpm 6662   RRcr 7823   0cc0 7824   1c1 7825    + caddc 7827    <_ cle 8006    - cmin 8141   NN0cn0 9189   ZZcz 9266   ZZ>=cuz 9541    seqcseq 10458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-addcom 7924  ax-addass 7926  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-0id 7932  ax-rnegex 7933  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-ltadd 7940
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-frec 6405  df-pm 6664  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-inn 8933  df-n0 9190  df-z 9267  df-uz 9542  df-seqfrec 10459
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator