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

Definition df-nninf 6770
Description: Define the set of nonincreasing sequences in  2o  ^m  om. Definition in Section 3.1 of [Pierik], p. 15. If we assumed excluded middle, this would be essentially the same as NN0* as defined at df-xnn0 8707 but in its absence the relationship between the two is more complicated. This definition would function much the same whether we used  om or  NN0, but the former allows us to take advantage of  2o  =  { (/)
,  1o } (df2o3 6177) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.)
Assertion
Ref Expression
df-nninf  |-  =  { f  e.  ( 2o  ^m  om )  |  A. i  e.  om  ( f `  suc  i )  C_  (
f `  i ) }
Distinct variable group:    f, i

Detailed syntax breakdown of Definition df-nninf
StepHypRef Expression
1 xnninf 6768 . 2  class
2 vi . . . . . . . 8  setvar  i
32cv 1288 . . . . . . 7  class  i
43csuc 4183 . . . . . 6  class  suc  i
5 vf . . . . . . 7  setvar  f
65cv 1288 . . . . . 6  class  f
74, 6cfv 5002 . . . . 5  class  ( f `
 suc  i )
83, 6cfv 5002 . . . . 5  class  ( f `
 i )
97, 8wss 2997 . . . 4  wff  ( f `
 suc  i )  C_  ( f `  i
)
10 com 4395 . . . 4  class  om
119, 2, 10wral 2359 . . 3  wff  A. i  e.  om  ( f `  suc  i )  C_  (
f `  i )
12 c2o 6157 . . . 4  class  2o
13 cmap 6385 . . . 4  class  ^m
1412, 10, 13co 5634 . . 3  class  ( 2o 
^m  om )
1511, 5, 14crab 2363 . 2  class  { f  e.  ( 2o  ^m  om )  |  A. i  e.  om  ( f `  suc  i )  C_  (
f `  i ) }
161, 15wceq 1289 1  wff  =  { f  e.  ( 2o  ^m  om )  |  A. i  e.  om  ( f `  suc  i )  C_  (
f `  i ) }
Colors of variables: wff set class
This definition is referenced by:  infnninf  6784  nnnninf  6785  0nninf  11550  nninff  11551  nnsf  11552  peano4nninf  11553  nninfalllemn  11555  nninfalllem1  11556  nninfex  11558  nninfself  11562
  Copyright terms: Public domain W3C validator