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

Definition df-nninf 7058
 Description: Define the set of nonincreasing sequences in . 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 9148 but in its absence the relationship between the two is more complicated. This definition would function much the same whether we used or , but the former allows us to take advantage of (df2o3 6374) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.)
Assertion
Ref Expression
df-nninf
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-nninf
StepHypRef Expression
1 xnninf 7057 . 2
2 vi . . . . . . . 8
32cv 1334 . . . . . . 7
43csuc 4325 . . . . . 6
5 vf . . . . . . 7
65cv 1334 . . . . . 6
74, 6cfv 5169 . . . . 5
83, 6cfv 5169 . . . . 5
97, 8wss 3102 . . . 4
10 com 4548 . . . 4
119, 2, 10wral 2435 . . 3
12 c2o 6354 . . . 4
13 cmap 6590 . . . 4
1412, 10, 13co 5821 . . 3
1511, 5, 14crab 2439 . 2
161, 15wceq 1335 1
 Colors of variables: wff set class This definition is referenced by:  nninfex  7059  nninff  7060  infnninf  7061  infnninfOLD  7062  nnnninf  7063  nnnninfeq  7065  nnnninfeq2  7066  0nninf  13547  nnsf  13548  peano4nninf  13549  nninfalllem1  13551  nninfself  13556
 Copyright terms: Public domain W3C validator