Theorem dfz12s2

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	dfz12s2	|- ZZ_s[1/2] = ( _Old ` _om )

Proof

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