Definition df-nninf 7181

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 9307 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 6485) 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 7180	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1363	. . . . . . 7 class i
4	3	csuc 4397	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1363	. . . . . 6 class f
7	4, 6	cfv 5255	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5255	. . . . 5 class ( f ` i )
9	7, 8	wss 3154	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4623	. . . 4 class om
11	9, 2, 10	wral 2472	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6465	. . . 4 class 2o
13		cmap 6704	. . . 4 class ^m
14	12, 10, 13	co 5919	. . 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  7182  nninff  7183  nninfninc  7184  infnninf  7185  infnninfOLD  7186  nnnninf  7187  nnnninfeq  7189  nnnninfeq2  7190  nninfwlpoimlemg  7236  0nninf  15564  nnsf  15565  peano4nninf  15566  nninfalllem1  15568  nninfself  15573