Definition df-nninf 7015

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 9065 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 6335) 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 7013	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1331	. . . . . . 7 class i
4	3	csuc 4295	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1331	. . . . . 6 class f
7	4, 6	cfv 5131	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5131	. . . . 5 class ( f ` i )
9	7, 8	wss 3076	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4512	. . . 4 class om
11	9, 2, 10	wral 2417	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6315	. . . 4 class 2o
13		cmap 6550	. . . 4 class ^m
14	12, 10, 13	co 5782	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2421	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1332	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  infnninf  7030  nnnninf  7031  0nninf  13372  nninff  13373  nnsf  13374  peano4nninf  13375  nninfalllemn  13377  nninfalllem1  13378  nninfex  13380  nninfself  13384