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

Definition df-nninf 7121
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 9242 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 6433) 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 7120 . 2  class
2 vi . . . . . . . 8  setvar  i
32cv 1352 . . . . . . 7  class  i
43csuc 4367 . . . . . 6  class  suc  i
5 vf . . . . . . 7  setvar  f
65cv 1352 . . . . . 6  class  f
74, 6cfv 5218 . . . . 5  class  ( f `
 suc  i )
83, 6cfv 5218 . . . . 5  class  ( f `
 i )
97, 8wss 3131 . . . 4  wff  ( f `
 suc  i )  C_  ( f `  i
)
10 com 4591 . . . 4  class  om
119, 2, 10wral 2455 . . 3  wff  A. i  e.  om  ( f `  suc  i )  C_  (
f `  i )
12 c2o 6413 . . . 4  class  2o
13 cmap 6650 . . . 4  class  ^m
1412, 10, 13co 5877 . . 3  class  ( 2o 
^m  om )
1511, 5, 14crab 2459 . 2  class  { f  e.  ( 2o  ^m  om )  |  A. i  e.  om  ( f `  suc  i )  C_  (
f `  i ) }
161, 15wceq 1353 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:  nninfex  7122  nninff  7123  infnninf  7124  infnninfOLD  7125  nnnninf  7126  nnnninfeq  7128  nnnninfeq2  7129  nninfwlpoimlemg  7175  0nninf  14792  nnsf  14793  peano4nninf  14794  nninfalllem1  14796  nninfself  14801
  Copyright terms: Public domain W3C validator