Definition df-nninf 7362

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 9510 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 6640) 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 7361	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1397	. . . . . . 7 class i
4	3	csuc 4468	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1397	. . . . . 6 class f
7	4, 6	cfv 5333	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5333	. . . . 5 class ( f ` i )
9	7, 8	wss 3201	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4694	. . . 4 class om
11	9, 2, 10	wral 2511	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6619	. . . 4 class 2o
13		cmap 6860	. . . 4 class ^m
14	12, 10, 13	co 6028	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2515	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1398	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7363  nninff  7364  nninfninc  7365  infnninf  7366  infnninfOLD  7367  nnnninf  7368  nnnninfeq  7370  nnnninfeq2  7371  nninfwlpoimlemg  7417  0nninf  16713  nnsf  16714  peano4nninf  16715  nninfalllem1  16717  nninfself  16722