Definition df-nninf 7318

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 9465 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 6596) 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

Step	Hyp	Ref	Expression
1		xnninf 7317	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1396	. . . . . . 7 class i
4	3	csuc 4462	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1396	. . . . . 6 class f
7	4, 6	cfv 5326	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5326	. . . . 5 class ( f ` i )
9	7, 8	wss 3200	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4688	. . . 4 class om
11	9, 2, 10	wral 2510	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6575	. . . 4 class 2o
13		cmap 6816	. . . 4 class ^m
14	12, 10, 13	co 6017	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2514	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1397	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7319  nninff  7320  nninfninc  7321  infnninf  7322  infnninfOLD  7323  nnnninf  7324  nnnninfeq  7326  nnnninfeq2  7327  nninfwlpoimlemg  7373  0nninf  16606  nnsf  16607  peano4nninf  16608  nninfalllem1  16610  nninfself  16615