Definition df-nninf 7118

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 9239 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 6430) 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 7117	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1352	. . . . . . 7 class i
4	3	csuc 4365	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1352	. . . . . 6 class f
7	4, 6	cfv 5216	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5216	. . . . 5 class ( f ` i )
9	7, 8	wss 3129	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4589	. . . 4 class om
11	9, 2, 10	wral 2455	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6410	. . . 4 class 2o
13		cmap 6647	. . . 4 class ^m
14	12, 10, 13	co 5874	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2459	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1353	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7119  nninff  7120  infnninf  7121  infnninfOLD  7122  nnnninf  7123  nnnninfeq  7125  nnnninfeq2  7126  nninfwlpoimlemg  7172  0nninf  14723  nnsf  14724  peano4nninf  14725  nninfalllem1  14727  nninfself  14732