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	Could not format assertion : No typesetting found for |- ZZ_s[1/2] = { x | E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czs12	Could not format ZZ_s[1/2] : No typesetting found for class ZZ_s[1/2] with typecode class
1		vx	$$setvarx$$
2		vy	$$setvary$$
3		czs	$$class{\mathbb{Z}}_s$$
4		vz	$$setvarz$$
5		cnn0s	$$class{\mathbb{N}}_{\mathrm{0s}}$$
6	1	cv	$$setvarx$$
7	2	cv	$$setvary$$
8		cdivs	$$class{/}_{\mathrm{su}}$$
9		c2s	Could not format 2s : No typesetting found for class 2s with typecode class
10		cexps	Could not format ^su : No typesetting found for class ^su with typecode class
11	4	cv	$$setvarz$$
12	9 11 10	co	Could not format ( 2s ^su z ) : No typesetting found for class ( 2s ^su z ) with typecode class
13	7 12 8	co	Could not format ( y /su ( 2s ^su z ) ) : No typesetting found for class ( y /su ( 2s ^su z ) ) with typecode class
14	6 13	wceq	Could not format x = ( y /su ( 2s ^su z ) ) : No typesetting found for wff x = ( y /su ( 2s ^su z ) ) with typecode wff
15	14 4 5	wrex	Could not format E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) : No typesetting found for wff E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) with typecode wff
16	15 2 3	wrex	Could not format E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) : No typesetting found for wff E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) with typecode wff
17	16 1	cab	Could not format { x | E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) } : No typesetting found for class { x | E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) } with typecode class
18	0 17	wceq	Could not format ZZ_s[1/2] = { x | E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) } : No typesetting found for wff ZZ_s[1/2] = { x | E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) } with typecode wff