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

Definition df-nninf 6973
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 8992 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 6293) 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 6971 . 2  class
2 vi . . . . . . . 8  setvar  i
32cv 1313 . . . . . . 7  class  i
43csuc 4255 . . . . . 6  class  suc  i
5 vf . . . . . . 7  setvar  f
65cv 1313 . . . . . 6  class  f
74, 6cfv 5091 . . . . 5  class  ( f `
 suc  i )
83, 6cfv 5091 . . . . 5  class  ( f `
 i )
97, 8wss 3039 . . . 4  wff  ( f `
 suc  i )  C_  ( f `  i
)
10 com 4472 . . . 4  class  om
119, 2, 10wral 2391 . . 3  wff  A. i  e.  om  ( f `  suc  i )  C_  (
f `  i )
12 c2o 6273 . . . 4  class  2o
13 cmap 6508 . . . 4  class  ^m
1412, 10, 13co 5740 . . 3  class  ( 2o 
^m  om )
1511, 5, 14crab 2395 . 2  class  { f  e.  ( 2o  ^m  om )  |  A. i  e.  om  ( f `  suc  i )  C_  (
f `  i ) }
161, 15wceq 1314 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  6988  nnnninf  6989  0nninf  12999  nninff  13000  nnsf  13001  peano4nninf  13002  nninfalllemn  13004  nninfalllem1  13005  nninfex  13007  nninfself  13011
  Copyright terms: Public domain W3C validator