Definition df-nninf 7460

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 9631 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 6702) 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 7459	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1401	. . . . . . 7 class i
4	3	csuc 4510	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1401	. . . . . 6 class f
7	4, 6	cfv 5377	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5377	. . . . 5 class ( f ` i )
9	7, 8	wss 3220	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4737	. . . 4 class om
11	9, 2, 10	wral 2528	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6681	. . . 4 class 2o
13		cmap 6922	. . . 4 class ^m
14	12, 10, 13	co 6085	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2532	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1402	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is used by:  nninfex  7461  nninff  7462  nninfninc  7463  infnninf  7464  infnninfOLD  7465  nnnninf  7466  nnnninfeq  7468  nnnninfeq2  7469  nninfwlpoimlemg  7515  0nninf  17047  nnsf  17048  peano4nninf  17049  nninfalllem1  17051  nninfself  17056