Definition df-nninf 7287

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 9433 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 6576) 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 7286	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1394	. . . . . . 7 class i
4	3	csuc 4456	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1394	. . . . . 6 class f
7	4, 6	cfv 5318	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5318	. . . . 5 class ( f ` i )
9	7, 8	wss 3197	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4682	. . . 4 class om
11	9, 2, 10	wral 2508	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6556	. . . 4 class 2o
13		cmap 6795	. . . 4 class ^m
14	12, 10, 13	co 6001	. . 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  7288  nninff  7289  nninfninc  7290  infnninf  7291  infnninfOLD  7292  nnnninf  7293  nnnninfeq  7295  nnnninfeq2  7296  nninfwlpoimlemg  7342  0nninf  16370  nnsf  16371  peano4nninf  16372  nninfalllem1  16374  nninfself  16379