Definition df-nninf 7466

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 9642 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 6706) 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 7465	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1401	. . . . . . 7 class i
4	3	csuc 4512	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1401	. . . . . 6 class f
7	4, 6	cfv 5380	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5380	. . . . 5 class ( f ` i )
9	7, 8	wss 3220	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4739	. . . 4 class om
11	9, 2, 10	wral 2528	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6685	. . . 4 class 2o
13		cmap 6926	. . . 4 class ^m
14	12, 10, 13	co 6088	. . 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  7467  nninff  7468  nninfninc  7469  infnninf  7470  infnninfOLD  7471  nnnninf  7472  nnnninfeq  7474  nnnninfeq2  7475  nninfwlpoimlemg  7521  0nninf  17253  nnsf  17254  peano4nninf  17255  nninfalllem1  17257  nninfself  17262