Definition df-nninf 7085

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 9178 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 6398) 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 7084	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1342	. . . . . . 7 class i
4	3	csuc 4343	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1342	. . . . . 6 class f
7	4, 6	cfv 5188	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5188	. . . . 5 class ( f ` i )
9	7, 8	wss 3116	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4567	. . . 4 class om
11	9, 2, 10	wral 2444	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6378	. . . 4 class 2o
13		cmap 6614	. . . 4 class ^m
14	12, 10, 13	co 5842	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2448	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1343	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7086  nninff  7087  infnninf  7088  infnninfOLD  7089  nnnninf  7090  nnnninfeq  7092  nnnninfeq2  7093  0nninf  13884  nnsf  13885  peano4nninf  13886  nninfalllem1  13888  nninfself  13893