Definition df-z12s 28801

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 28800	. 2 class ℤs[1/2]
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1568	. . . . . 6 class 𝑥
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1568	. . . . . . 7 class 𝑦
6		c2s 28796	. . . . . . . 8 class 2s
7		vz	. . . . . . . . 9 setvar 𝑧
8	7	cv 1568	. . . . . . . 8 class 𝑧
9		cexps 28798	. . . . . . . 8 class ↑s
10	6, 8, 9	co 7420	. . . . . . 7 class (2s↑s𝑧)
11		cdivs 28573	. . . . . . 7 class /su
12	5, 10, 11	co 7420	. . . . . 6 class (𝑦 /su (2s↑s𝑧))
13	3, 12	wceq 1569	. . . . 5 wff 𝑥 = (𝑦 /su (2s↑s𝑧))
14		cn0s 28698	. . . . 5 class ℕ0s
15	13, 7, 14	wrex 3086	. . . 4 wff ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))
16		czs 28764	. . . 4 class ℤs
17	15, 4, 16	wrex 3086	. . 3 wff ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))
18	17, 2	cab 2738	. 2 class {𝑥 ∣ ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))}
19	1, 18	wceq 1569	1 wff ℤs[1/2] = {𝑥 ∣ ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))}

This definition is used by:  elz12s  28858  z12sex  28860