Definition df-zs12

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czs12	⊢ ℤs[1/2]
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3		czs	⊢ ℤs
4		vz	⊢ 𝑧
5		cnn0s	⊢ ℕ0s
6	1	cv	⊢ 𝑥
7	2	cv	⊢ 𝑦
8		cdivs	⊢ /su
9		c2s	⊢ 2s
10		cexps	⊢ ↑s
11	4	cv	⊢ 𝑧
12	9 11 10	co	⊢ ( 2s ↑s 𝑧 )
13	7 12 8	co	⊢ ( 𝑦 /su ( 2s ↑s 𝑧 ) )
14	6 13	wceq	⊢ 𝑥 = ( 𝑦 /su ( 2s ↑s 𝑧 ) )
15	14 4 5	wrex	⊢ ∃ 𝑧 ∈ ℕ0s 𝑥 = ( 𝑦 /su ( 2s ↑s 𝑧 ) )
16	15 2 3	wrex	⊢ ∃ 𝑦 ∈ ℤs ∃ 𝑧 ∈ ℕ0s 𝑥 = ( 𝑦 /su ( 2s ↑s 𝑧 ) )
17	16 1	cab	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℤs ∃ 𝑧 ∈ ℕ0s 𝑥 = ( 𝑦 /su ( 2s ↑s 𝑧 ) ) }
18	0 17	wceq	⊢ ℤs[1/2] = { 𝑥 ∣ ∃ 𝑦 ∈ ℤs ∃ 𝑧 ∈ ℕ0s 𝑥 = ( 𝑦 /su ( 2s ↑s 𝑧 ) ) }