Definition df-nninf 7424

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 9581 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 6675) 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 7423	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1397	. . . . . . 7 class i
4	3	csuc 4491	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1397	. . . . . 6 class f
7	4, 6	cfv 5357	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5357	. . . . 5 class ( f ` i )
9	7, 8	wss 3214	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4717	. . . 4 class om
11	9, 2, 10	wral 2522	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6654	. . . 4 class 2o
13		cmap 6895	. . . 4 class ^m
14	12, 10, 13	co 6058	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2526	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1398	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7425  nninff  7426  nninfninc  7427  infnninf  7428  infnninfOLD  7429  nnnninf  7430  nnnninfeq  7432  nnnninfeq2  7433  nninfwlpoimlemg  7479  0nninf  16908  nnsf  16909  peano4nninf  16910  nninfalllem1  16912  nninfself  16917