Definition df-nninf 7097

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 9199 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 6409) 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 7096	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1347	. . . . . . 7 class i
4	3	csuc 4350	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1347	. . . . . 6 class f
7	4, 6	cfv 5198	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5198	. . . . 5 class ( f ` i )
9	7, 8	wss 3121	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4574	. . . 4 class om
11	9, 2, 10	wral 2448	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6389	. . . 4 class 2o
13		cmap 6626	. . . 4 class ^m
14	12, 10, 13	co 5853	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2452	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1348	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7098  nninff  7099  infnninf  7100  infnninfOLD  7101  nnnninf  7102  nnnninfeq  7104  nnnninfeq2  7105  nninfwlpoimlemg  7151  0nninf  14037  nnsf  14038  peano4nninf  14039  nninfalllem1  14041  nninfself  14046