Definition df-nninf 7058

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 9148 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 6374) 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 7057	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1334	. . . . . . 7 class i
4	3	csuc 4325	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1334	. . . . . 6 class f
7	4, 6	cfv 5169	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5169	. . . . 5 class ( f ` i )
9	7, 8	wss 3102	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4548	. . . 4 class om
11	9, 2, 10	wral 2435	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6354	. . . 4 class 2o
13		cmap 6590	. . . 4 class ^m
14	12, 10, 13	co 5821	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2439	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1335	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7059  nninff  7060  infnninf  7061  infnninfOLD  7062  nnnninf  7063  nnnninfeq  7065  nnnninfeq2  7066  0nninf  13547  nnsf  13548  peano4nninf  13549  nninfalllem1  13551  nninfself  13556