Definition df-nninf 7255

Description: Define the set of nonincreasing sequences in 2_o ↑_𝑚 ω. Definition in Section 3.1 of [Pierik], p. 15. If we assumed excluded middle, this would be essentially the same as ℕ₀^* as defined at df-xnn0 9401 but in its absence the relationship between the two is more complicated. This definition would function much the same whether we used ω or ℕ₀, but the former allows us to take advantage of 2_o = {∅, 1_o} (df2o3 6546) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.)

Assertion

Ref	Expression
df-nninf	⊢ ℕ∞ = {𝑓 ∈ (2o ↑𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)}

Distinct variable group:   𝑓,𝑖

Detailed syntax breakdown of Definition df-nninf

Step	Hyp	Ref	Expression
1		xnninf 7254	. 2 class ℕ∞
2		vi	. . . . . . . 8 setvar 𝑖
3	2	cv 1374	. . . . . . 7 class 𝑖
4	3	csuc 4433	. . . . . 6 class suc 𝑖
5		vf	. . . . . . 7 setvar 𝑓
6	5	cv 1374	. . . . . 6 class 𝑓
7	4, 6	cfv 5294	. . . . 5 class (𝑓‘suc 𝑖)
8	3, 6	cfv 5294	. . . . 5 class (𝑓‘𝑖)
9	7, 8	wss 3177	. . . 4 wff (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)
10		com 4659	. . . 4 class ω
11	9, 2, 10	wral 2488	. . 3 wff ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)
12		c2o 6526	. . . 4 class 2o
13		cmap 6765	. . . 4 class ↑𝑚
14	12, 10, 13	co 5974	. . 3 class (2o ↑𝑚 ω)
15	11, 5, 14	crab 2492	. 2 class {𝑓 ∈ (2o ↑𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)}
16	1, 15	wceq 1375	1 wff ℕ∞ = {𝑓 ∈ (2o ↑𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)}

This definition is referenced by:  nninfex  7256  nninff  7257  nninfninc  7258  infnninf  7259  infnninfOLD  7260  nnnninf  7261  nnnninfeq  7263  nnnninfeq2  7264  nninfwlpoimlemg  7310  0nninf  16281  nnsf  16282  peano4nninf  16283  nninfalllem1  16285  nninfself  16290