Definition df-nninf 7411

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 9564 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 6662) 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 7410	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1397	. . . . . . 7 class i
4	3	csuc 4486	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1397	. . . . . 6 class f
7	4, 6	cfv 5352	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5352	. . . . 5 class ( f ` i )
9	7, 8	wss 3211	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4712	. . . 4 class om
11	9, 2, 10	wral 2520	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6641	. . . 4 class 2o
13		cmap 6882	. . . 4 class ^m
14	12, 10, 13	co 6050	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2524	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1398	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7412  nninff  7413  nninfninc  7414  infnninf  7415  infnninfOLD  7416  nnnninf  7417  nnnninfeq  7419  nnnninfeq2  7420  nninfwlpoimlemg  7466  0nninf  16782  nnsf  16783  peano4nninf  16784  nninfalllem1  16786  nninfself  16791