Definition df-nninf 7283

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 9429 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 6574) 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 7282	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1394	. . . . . . 7 class i
4	3	csuc 4455	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1394	. . . . . 6 class f
7	4, 6	cfv 5317	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5317	. . . . 5 class ( f ` i )
9	7, 8	wss 3197	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4681	. . . 4 class om
11	9, 2, 10	wral 2508	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6554	. . . 4 class 2o
13		cmap 6793	. . . 4 class ^m
14	12, 10, 13	co 6000	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2512	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1395	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7284  nninff  7285  nninfninc  7286  infnninf  7287  infnninfOLD  7288  nnnninf  7289  nnnninfeq  7291  nnnninfeq2  7292  nninfwlpoimlemg  7338  0nninf  16329  nnsf  16330  peano4nninf  16331  nninfalllem1  16333  nninfself  16338