Definition df-z12s 28411

Description: Define the set of dyadic rationals. This is the set of rationals whose denominator is a power of two. Later we will prove that this is precisely the set of surreals with a finite birthday. (Contributed by Scott Fenton, 27-May-2025.)

Assertion

Ref	Expression
df-z12s	⊢ ℤs[1/2] = {𝑥 ∣ ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))}

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-z12s

Step	Hyp	Ref	Expression
1		cz12s 28410	. 2 class ℤs[1/2]
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1540	. . . . . 6 class 𝑥
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1540	. . . . . . 7 class 𝑦
6		c2s 28406	. . . . . . . 8 class 2s
7		vz	. . . . . . . . 9 setvar 𝑧
8	7	cv 1540	. . . . . . . 8 class 𝑧
9		cexps 28408	. . . . . . . 8 class ↑s
10	6, 8, 9	co 7358	. . . . . . 7 class (2s↑s𝑧)
11		cdivs 28183	. . . . . . 7 class /su
12	5, 10, 11	co 7358	. . . . . 6 class (𝑦 /su (2s↑s𝑧))
13	3, 12	wceq 1541	. . . . 5 wff 𝑥 = (𝑦 /su (2s↑s𝑧))
14		cn0s 28308	. . . . 5 class ℕ0s
15	13, 7, 14	wrex 3060	. . . 4 wff ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))
16		czs 28374	. . . 4 class ℤs
17	15, 4, 16	wrex 3060	. . 3 wff ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))
18	17, 2	cab 2714	. 2 class {𝑥 ∣ ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))}
19	1, 18	wceq 1541	1 wff ℤs[1/2] = {𝑥 ∣ ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))}

This definition is referenced by:  elz12s  28468  z12sex  28470