Definition df-nninf 7319

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 9466 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 6597) 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 7318	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar i
3	2	cv 1396	. . . . . . 7 class i
4	3	csuc 4462	. . . . . 6 class suc i
5		vf	. . . . . . 7 setvar f
6	5	cv 1396	. . . . . 6 class f
7	4, 6	cfv 5326	. . . . 5 class ( f ` suc i )
8	3, 6	cfv 5326	. . . . 5 class ( f ` i )
9	7, 8	wss 3200	. . . 4 wff ( f ` suc i ) C_ ( f ` i )
10		com 4688	. . . 4 class om
11	9, 2, 10	wral 2510	. . 3 wff A. i e. om ( f ` suc i ) C_ ( f ` i )
12		c2o 6576	. . . 4 class 2o
13		cmap 6817	. . . 4 class ^m
14	12, 10, 13	co 6018	. . 3 class ( 2o ^m om )
15	11, 5, 14	crab 2514	. 2 class { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
16	1, 15	wceq 1397	1 wff ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }

This definition is referenced by:  nninfex  7320  nninff  7321  nninfninc  7322  infnninf  7323  infnninfOLD  7324  nnnninf  7325  nnnninfeq  7327  nnnninfeq2  7328  nninfwlpoimlemg  7374  0nninf  16657  nnsf  16658  peano4nninf  16659  nninfalllem1  16661  nninfself  16666