Definition df-nninf 7310

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 9456 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 6592) 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 7309	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1394	. . . . . . 7 class i
4	3	csuc 4460	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1394	. . . . . 6 class f
7	4, 6	cfv 5324	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5324	. . . . 5 class ( f ` i )
9	7, 8	wss 3198	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4686	. . . 4 class om
11	9, 2, 10	wral 2508	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6571	. . . 4 class 2o
13		cmap 6812	. . . 4 class ^m
14	12, 10, 13	co 6013	. . 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  7311  nninff  7312  nninfninc  7313  infnninf  7314  infnninfOLD  7315  nnnninf  7316  nnnninfeq  7318  nnnninfeq2  7319  nninfwlpoimlemg  7365  0nninf  16542  nnsf  16543  peano4nninf  16544  nninfalllem1  16546  nninfself  16551