Definition df-nninf 7450

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 9610 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 6692) 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 7449	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1401	. . . . . . 7 class i
4	3	csuc 4505	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1401	. . . . . 6 class f
7	4, 6	cfv 5372	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5372	. . . . 5 class ( f ` i )
9	7, 8	wss 3220	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4732	. . . 4 class om
11	9, 2, 10	wral 2528	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6671	. . . 4 class 2o
13		cmap 6912	. . . 4 class ^m
14	12, 10, 13	co 6075	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2532	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1402	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7451  nninff  7452  nninfninc  7453  infnninf  7454  infnninfOLD  7455  nnnninf  7456  nnnninfeq  7458  nnnninfeq2  7459  nninfwlpoimlemg  7505  0nninf  16952  nnsf  16953  peano4nninf  16954  nninfalllem1  16956  nninfself  16961