Definition df-zs12 28408

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-zs12	⊢ ℤs[1/2] = {𝑥 ∣ ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))}

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-zs12

Step	Hyp	Ref	Expression
1		czs12 28407	. 2 class ℤs[1/2]
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1536	. . . . . 6 class 𝑥
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1536	. . . . . . 7 class 𝑦
6		c2s 28403	. . . . . . . 8 class 2s
7		vz	. . . . . . . . 9 setvar 𝑧
8	7	cv 1536	. . . . . . . 8 class 𝑧
9		cexps 28405	. . . . . . . 8 class ↑s
10	6, 8, 9	co 7445	. . . . . . 7 class (2s↑s𝑧)
11		cdivs 28222	. . . . . . 7 class /su
12	5, 10, 11	co 7445	. . . . . 6 class (𝑦 /su (2s↑s𝑧))
13	3, 12	wceq 1537	. . . . 5 wff 𝑥 = (𝑦 /su (2s↑s𝑧))
14		cnn0s 28327	. . . . 5 class ℕ0s
15	13, 7, 14	wrex 3072	. . . 4 wff ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))
16		czs 28373	. . . 4 class ℤs
17	15, 4, 16	wrex 3072	. . 3 wff ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))
18	17, 2	cab 2711	. 2 class {𝑥 ∣ ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))}
19	1, 18	wceq 1537	1 wff ℤs[1/2] = {𝑥 ∣ ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))}

This definition is referenced by:  elzs12  28430  zs12ex  28431