Definition df-nninf 7007

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 9041 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 6327) 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 7005	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1330	. . . . . . 7 class i
4	3	csuc 4287	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1330	. . . . . 6 class f
7	4, 6	cfv 5123	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5123	. . . . 5 class ( f ` i )
9	7, 8	wss 3071	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4504	. . . 4 class om
11	9, 2, 10	wral 2416	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6307	. . . 4 class 2o
13		cmap 6542	. . . 4 class ^m
14	12, 10, 13	co 5774	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2420	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1331	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  infnninf  7022  nnnninf  7023  0nninf  13197  nninff  13198  nnsf  13199  peano4nninf  13200  nninfalllemn  13202  nninfalllem1  13203  nninfex  13205  nninfself  13209