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

Theorem ennnfonelemkh 11936
Description: Lemma for ennnfone 11949. 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 5421 . . . . . . 7  |-  ( w  =  0  ->  ( H `  w )  =  ( H ` 
0 ) )
32dmeqd 4741 . . . . . 6  |-  ( w  =  0  ->  dom  ( H `  w )  =  dom  ( H `
 0 ) )
4 fveq2 5421 . . . . . 6  |-  ( w  =  0  ->  ( `' N `  w )  =  ( `' N `  0 ) )
53, 4sseq12d 3128 . . . . 5  |-  ( w  =  0  ->  ( dom  ( H `  w
)  C_  ( `' N `  w )  <->  dom  ( H `  0
)  C_  ( `' N `  0 )
) )
65imbi2d 229 . . . 4  |-  ( w  =  0  ->  (
( ph  ->  dom  ( H `  w )  C_  ( `' N `  w ) )  <->  ( ph  ->  dom  ( H ` 
0 )  C_  ( `' N `  0 ) ) ) )
7 fveq2 5421 . . . . . . 7  |-  ( w  =  m  ->  ( H `  w )  =  ( H `  m ) )
87dmeqd 4741 . . . . . 6  |-  ( w  =  m  ->  dom  ( H `  w )  =  dom  ( H `
 m ) )
9 fveq2 5421 . . . . . 6  |-  ( w  =  m  ->  ( `' N `  w )  =  ( `' N `  m ) )
108, 9sseq12d 3128 . . . . 5  |-  ( w  =  m  ->  ( dom  ( H `  w
)  C_  ( `' N `  w )  <->  dom  ( H `  m
)  C_  ( `' N `  m )
) )
1110imbi2d 229 . . . 4  |-  ( w  =  m  ->  (
( ph  ->  dom  ( H `  w )  C_  ( `' N `  w ) )  <->  ( ph  ->  dom  ( H `  m )  C_  ( `' N `  m ) ) ) )
12 fveq2 5421 . . . . . . 7  |-  ( w  =  ( m  + 
1 )  ->  ( H `  w )  =  ( H `  ( m  +  1
) ) )
1312dmeqd 4741 . . . . . 6  |-  ( w  =  ( m  + 
1 )  ->  dom  ( H `  w )  =  dom  ( H `
 ( m  + 
1 ) ) )
14 fveq2 5421 . . . . . 6  |-  ( w  =  ( m  + 
1 )  ->  ( `' N `  w )  =  ( `' N `  ( m  +  1 ) ) )
1513, 14sseq12d 3128 . . . . 5  |-  ( w  =  ( m  + 
1 )  ->  ( dom  ( H `  w
)  C_  ( `' N `  w )  <->  dom  ( H `  (
m  +  1 ) )  C_  ( `' N `  ( m  +  1 ) ) ) )
1615imbi2d 229 . . . 4  |-  ( w  =  ( m  + 
1 )  ->  (
( ph  ->  dom  ( H `  w )  C_  ( `' N `  w ) )  <->  ( ph  ->  dom  ( H `  ( m  +  1
) )  C_  ( `' N `  ( m  +  1 ) ) ) ) )
17 fveq2 5421 . . . . . . 7  |-  ( w  =  P  ->  ( H `  w )  =  ( H `  P ) )
1817dmeqd 4741 . . . . . 6  |-  ( w  =  P  ->  dom  ( H `  w )  =  dom  ( H `
 P ) )
19 fveq2 5421 . . . . . 6  |-  ( w  =  P  ->  ( `' N `  w )  =  ( `' N `  P ) )
2018, 19sseq12d 3128 . . . . 5  |-  ( w  =  P  ->  ( dom  ( H `  w
)  C_  ( `' N `  w )  <->  dom  ( H `  P
)  C_  ( `' N `  P )
) )
2120imbi2d 229 . . . 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 11929 . . . . . . . 8  |-  ( ph  ->  ( H `  0
)  =  (/) )
3029dmeqd 4741 . . . . . . 7  |-  ( ph  ->  dom  ( H ` 
0 )  =  dom  (/) )
31 dm0 4753 . . . . . . 7  |-  dom  (/)  =  (/)
3230, 31syl6eq 2188 . . . . . 6  |-  ( ph  ->  dom  ( H ` 
0 )  =  (/) )
33 0ss 3401 . . . . . 6  |-  (/)  C_  ( `' N `  0 )
3432, 33eqsstrdi 3149 . . . . 5  |-  ( ph  ->  dom  ( H ` 
0 )  C_  ( `' N `  0 ) )
3534a1i 9 . . . 4  |-  ( 0  e.  ZZ  ->  ( ph  ->  dom  ( H `  0 )  C_  ( `' N `  0 ) ) )
3626frechashgf1o 10213 . . . . . . . . . . . . . 14  |-  N : om
-1-1-onto-> NN0
37 f1of 5367 . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y
)
4023ad2antrr 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  F : om -onto-> A )
4124ad2antrr 479 . . . . . . . . . . . . . . 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 519 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  m  e.  ( ZZ>= `  0 )
)
43 nn0uz 9372 . . . . . . . . . . . . . . . . 17  |-  NN0  =  ( ZZ>= `  0 )
4442, 43eleqtrrdi 2233 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  m  e.  NN0 )
45 peano2nn0 9029 . . . . . . . . . . . . . . . 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 11932 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  dom  ( H `
 ( m  + 
1 ) )  e. 
om )
4847adantr 274 . . . . . . . . . . . . 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, 48ffvelrnd 5556 . . . . . . . . . . . 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 9043 . . . . . . . . . . 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 9043 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  m  e.  RR )
5251adantr 274 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  ( F `  ( `' N `  m ) )  e.  ( F " ( `' N `  m ) ) )  ->  m  e.  RR )
53 peano2re 7910 . . . . . . . . . . . 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 11930 . . . . . . . . . . . . . . . 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 274 . . . . . . . . . . . . . . 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 109 . . . . . . . . . . . . . . . 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 3481 . . . . . . . . . . . . . . 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 2172 . . . . . . . . . . . . . 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 4741 . . . . . . . . . . . . 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 5425 . . . . . . . . . . . 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 109 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  dom  ( H `
 m )  C_  ( `' N `  m ) )
63 0zd 9078 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  0  e.  ZZ )
6439, 40, 41, 25, 26, 27, 28, 44ennnfonelemom 11932 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  dom  ( H `
 m )  e. 
om )
65 f1ocnv 5380 . . . . . . . . . . . . . . . . . . . 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 5367 . . . . . . . . . . . . . . . . . . 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, 69ffvelrnd 5556 . . . . . . . . . . . . . . . . 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 10214 . . . . . . . . . . . . . . 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 146 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( N `  dom  ( H `  m ) )  <_ 
( N `  ( `' N `  m ) ) )
74 f1ocnvfv2 5679 . . . . . . . . . . . . . . 15  |-  ( ( N : om -1-1-onto-> NN0  /\  m  e. 
NN0 )  ->  ( N `  ( `' N `  m )
)  =  m )
7536, 44, 74sylancr 410 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( N `  ( `' N `  m ) )  =  m )
7673, 75breqtrd 3954 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( N `  dom  ( H `  m ) )  <_  m )
7776adantr 274 . . . . . . . . . . . 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 3950 . . . . . . . . . . 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 8701 . . . . . . . . . . 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 7898 . . . . . . . . . 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 5679 . . . . . . . . . . . 12  |-  ( ( N : om -1-1-onto-> NN0  /\  ( m  +  1 )  e. 
NN0 )  ->  ( N `  ( `' N `  ( m  +  1 ) ) )  =  ( m  +  1 ) )
8236, 46, 81sylancr 410 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( N `  ( `' N `  ( m  +  1
) ) )  =  ( m  +  1 ) )
8382adantr 274 . . . . . . . . . 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 3956 . . . . . . . . 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, 46ffvelrnd 5556 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( `' N `  ( m  +  1 ) )  e.  om )
8763, 26, 47, 86frec2uzled 10214 . . . . . . . . . 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 274 . . . . . . . . 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 166 . . . . . . . 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 274 . . . . . . . . . . . . . . . . . 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 109 . . . . . . . . . . . . . . . . . . 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 3484 . . . . . . . . . . . . . . . . . 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 2172 . . . . . . . . . . . . . . . . 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 4741 . . . . . . . . . . . . . . . 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 4746 . . . . . . . . . . . . . . . 16  |-  dom  (
( H `  m
)  u.  { <. dom  ( H `  m
) ,  ( F `
 ( `' N `  m ) ) >. } )  =  ( dom  ( H `  m )  u.  dom  {
<. dom  ( H `  m ) ,  ( F `  ( `' N `  m ) ) >. } )
9694, 95syl6eq 2188 . . . . . . . . . . . . . . 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 5345 . . . . . . . . . . . . . . . . . . . 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, 71ffvelrnd 5556 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  ( F `  ( `' N `  m ) )  e.  A )
10099adantr 274 . . . . . . . . . . . . . . . . 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 5010 . . . . . . . . . . . . . . . . 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 3230 . . . . . . . . . . . . . . 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 2172 . . . . . . . . . . . . . 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 4293 . . . . . . . . . . . . . 14  |-  suc  dom  ( H `  m )  =  ( dom  ( H `  m )  u.  { dom  ( H `
 m ) } )
106104, 105eqtr4di 2190 . . . . . . . . . . . . 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 519 . . . . . . . . . . . . . 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 274 . . . . . . . . . . . . . . 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 6388 . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . 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 146 . . . . . . . . . . . . 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 3133 . . . . . . . . . . . 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 9078 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  0  e.  ZZ )
11447adantr 274 . . . . . . . . . . . . 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 4509 . . . . . . . . . . . . . 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 10214 . . . . . . . . . . . 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 146 . . . . . . . . . . 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 10186 . . . . . . . . . . . 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 274 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= ` 
0 ) )  /\  dom  ( H `  m
)  C_  ( `' N `  m )
)  /\  -.  ( F `  ( `' N `  m )
)  e.  ( F
" ( `' N `  m ) ) )  ->  ( N `  ( `' N `  m ) )  =  m )
121120oveq1d 5789 . . . . . . . . . . . 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 2172 . . . . . . . . . . 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 3954 . . . . . . . . . 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 274 . . . . . . . . . 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 3956 . . . . . . . . 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 274 . . . . . . . . . 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 10214 . . . . . . . . 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 166 . . . . . . . 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 11923 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  -> DECID  ( F `  ( `' N `  m ) )  e.  ( F
" ( `' N `  m ) ) )
130 exmiddc 821 . . . . . . . . 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 787 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  0 )
)  /\  dom  ( H `
 m )  C_  ( `' N `  m ) )  ->  dom  ( H `
 ( m  + 
1 ) )  C_  ( `' N `  ( m  +  1 ) ) )
133132ex 114 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  0 )
)  ->  ( dom  ( H `  m ) 
C_  ( `' N `  m )  ->  dom  ( H `  ( m  +  1 ) ) 
C_  ( `' N `  ( m  +  1 ) ) ) )
134133expcom 115 . . . . 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 9395 . . 3  |-  ( P  e.  ( ZZ>= `  0
)  ->  ( ph  ->  dom  ( H `  P )  C_  ( `' N `  P ) ) )
137136, 43eleq2s 2234 . 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 103    <-> wb 104    \/ wo 697  DECID wdc 819    = wceq 1331    e. wcel 1480    =/= wne 2308   A.wral 2416   E.wrex 2417    u. cun 3069    C_ wss 3071   (/)c0 3363   ifcif 3474   {csn 3527   <.cop 3530   class class class wbr 3929    |-> cmpt 3989   suc csuc 4287   omcom 4504   `'ccnv 4538   dom cdm 4539   "cima 4542   -->wf 5119   -onto->wfo 5121   -1-1-onto->wf1o 5122   ` cfv 5123  (class class class)co 5774    e. cmpo 5776  freccfrec 6287    ^pm cpm 6543   RRcr 7631   0cc0 7632   1c1 7633    + caddc 7635    <_ cle 7813    - cmin 7945   NN0cn0 8989   ZZcz 9066   ZZ>=cuz 9338    seqcseq 10230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7723  ax-resscn 7724  ax-1cn 7725  ax-1re 7726  ax-icn 7727  ax-addcl 7728  ax-addrcl 7729  ax-mulcl 7730  ax-addcom 7732  ax-addass 7734  ax-distr 7736  ax-i2m1 7737  ax-0lt1 7738  ax-0id 7740  ax-rnegex 7741  ax-cnre 7743  ax-pre-ltirr 7744  ax-pre-ltwlin 7745  ax-pre-lttrn 7746  ax-pre-ltadd 7748
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-pm 6545  df-pnf 7814  df-mnf 7815  df-xr 7816  df-ltxr 7817  df-le 7818  df-sub 7947  df-neg 7948  df-inn 8733  df-n0 8990  df-z 9067  df-uz 9339  df-seqfrec 10231
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator