Definition df-nninf 7195

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 9330 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 6497) 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 7194	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1363	. . . . . . 7 class i
4	3	csuc 4401	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1363	. . . . . 6 class f
7	4, 6	cfv 5259	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5259	. . . . 5 class ( f ` i )
9	7, 8	wss 3157	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4627	. . . 4 class om
11	9, 2, 10	wral 2475	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6477	. . . 4 class 2o
13		cmap 6716	. . . 4 class ^m
14	12, 10, 13	co 5925	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2479	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1364	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7196  nninff  7197  nninfninc  7198  infnninf  7199  infnninfOLD  7200  nnnninf  7201  nnnninfeq  7203  nnnninfeq2  7204  nninfwlpoimlemg  7250  0nninf  15735  nnsf  15736  peano4nninf  15737  nninfalllem1  15739  nninfself  15744