Definition df-nninf 7122

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 9243 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 6434) 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 7121	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1352	. . . . . . 7 class i
4	3	csuc 4367	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1352	. . . . . 6 class f
7	4, 6	cfv 5218	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5218	. . . . 5 class ( f ` i )
9	7, 8	wss 3131	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4591	. . . 4 class om
11	9, 2, 10	wral 2455	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6414	. . . 4 class 2o
13		cmap 6651	. . . 4 class ^m
14	12, 10, 13	co 5878	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2459	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1353	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7123  nninff  7124  infnninf  7125  infnninfOLD  7126  nnnninf  7127  nnnninfeq  7129  nnnninfeq2  7130  nninfwlpoimlemg  7176  0nninf  14942  nnsf  14943  peano4nninf  14944  nninfalllem1  14946  nninfself  14951