Definition df-nninf 7186

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 9313 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 6488) 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 7185	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1363	. . . . . . 7 class i
4	3	csuc 4400	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1363	. . . . . 6 class f
7	4, 6	cfv 5258	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5258	. . . . 5 class ( f ` i )
9	7, 8	wss 3157	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4626	. . . 4 class om
11	9, 2, 10	wral 2475	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6468	. . . 4 class 2o
13		cmap 6707	. . . 4 class ^m
14	12, 10, 13	co 5922	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2479	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1364	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7187  nninff  7188  nninfninc  7189  infnninf  7190  infnninfOLD  7191  nnnninf  7192  nnnninfeq  7194  nnnninfeq2  7195  nninfwlpoimlemg  7241  0nninf  15648  nnsf  15649  peano4nninf  15650  nninfalllem1  15652  nninfself  15657