Theorem dfzs122

Description: The set of dyadic fractions is the same as the old set of _om . (Contributed by Scott Fenton, 26-Feb-2026)

	Ref	Expression
Assertion	dfzs122	|- ZZ_s[1/2] = ( _Old ` _om )

Proof

Step	Hyp	Ref	Expression
1		zs12no	|- ( x e. ZZ_s[1/2] -> x e. No )
2		oldssno	|- ( _Old ` _om ) C_ No
3	2	sseli	|- ( x e. ( _Old ` _om ) -> x e. No )
4		bdayfin	|- ( x e. No -> ( x e. ZZ_s[1/2] <-> ( bday ` x ) e. _om ) )
5		omelon	|- _om e. On
6		oldbday	|- ( ( _om e. On /\ x e. No ) -> ( x e. ( _Old ` _om ) <-> ( bday ` x ) e. _om ) )
7	5 6	mpan	|- ( x e. No -> ( x e. ( _Old ` _om ) <-> ( bday ` x ) e. _om ) )
8	4 7	bitr4d	|- ( x e. No -> ( x e. ZZ_s[1/2] <-> x e. ( _Old ` _om ) ) )
9	1 3 8	pm5.21nii	|- ( x e. ZZ_s[1/2] <-> x e. ( _Old ` _om ) )
10	9	eqriv	|- ZZ_s[1/2] = ( _Old ` _om )