Definition df-nninf 7236

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 9374 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 6528) 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 7235	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1372	. . . . . . 7 class i
4	3	csuc 4419	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1372	. . . . . 6 class f
7	4, 6	cfv 5279	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5279	. . . . 5 class ( f ` i )
9	7, 8	wss 3170	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4645	. . . 4 class om
11	9, 2, 10	wral 2485	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6508	. . . 4 class 2o
13		cmap 6747	. . . 4 class ^m
14	12, 10, 13	co 5956	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2489	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1373	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7237  nninff  7238  nninfninc  7239  infnninf  7240  infnninfOLD  7241  nnnninf  7242  nnnninfeq  7244  nnnninfeq2  7245  nninfwlpoimlemg  7291  0nninf  16076  nnsf  16077  peano4nninf  16078  nninfalllem1  16080  nninfself  16085