Definition df-nninf 7179

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 9304 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 6483) 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 7178	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1363	. . . . . . 7 class i
4	3	csuc 4396	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1363	. . . . . 6 class f
7	4, 6	cfv 5254	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5254	. . . . 5 class ( f ` i )
9	7, 8	wss 3153	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4622	. . . 4 class om
11	9, 2, 10	wral 2472	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6463	. . . 4 class 2o
13		cmap 6702	. . . 4 class ^m
14	12, 10, 13	co 5918	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2476	. 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  7180  nninff  7181  nninfninc  7182  infnninf  7183  infnninfOLD  7184  nnnninf  7185  nnnninfeq  7187  nnnninfeq2  7188  nninfwlpoimlemg  7234  0nninf  15494  nnsf  15495  peano4nninf  15496  nninfalllem1  15498  nninfself  15503