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	Could not format assertion : No typesetting found for |- ZZ_s[1/2] = ( _Old ` _om ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		z12no	Could not format ( x e. ZZ_s[1/2] -> x e. No ) : No typesetting found for |- ( x e. ZZ_s[1/2] -> x e. No ) with typecode |-
2		oldno	$$⊢x\in \mathrm{Old}\left(\mathrm{\omega }\right)\to x\in \mathrm{No}$$
3		bdayfin	Could not format ( x e. No -> ( x e. ZZ_s[1/2] <-> ( bday ` x ) e. _om ) ) : No typesetting found for |- ( x e. No -> ( x e. ZZ_s[1/2] <-> ( bday ` x ) e. _om ) ) with typecode |-
4		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
5		oldbday	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\wedge x\in \mathrm{No}\right)\to \left(x\in \mathrm{Old}\left(\mathrm{\omega }\right)\leftrightarrow \mathrm{bday}\left(x\right)\in \mathrm{\omega }\right)$$
6	4 5	mpan	$$⊢x\in \mathrm{No}\to \left(x\in \mathrm{Old}\left(\mathrm{\omega }\right)\leftrightarrow \mathrm{bday}\left(x\right)\in \mathrm{\omega }\right)$$
7	3 6	bitr4d	Could not format ( x e. No -> ( x e. ZZ_s[1/2] <-> x e. ( _Old ` _om ) ) ) : No typesetting found for |- ( x e. No -> ( x e. ZZ_s[1/2] <-> x e. ( _Old ` _om ) ) ) with typecode |-
8	1 2 7	pm5.21nii	Could not format ( x e. ZZ_s[1/2] <-> x e. ( _Old ` _om ) ) : No typesetting found for |- ( x e. ZZ_s[1/2] <-> x e. ( _Old ` _om ) ) with typecode |-
9	8	eqriv	Could not format ZZ_s[1/2] = ( _Old ` _om ) : No typesetting found for |- ZZ_s[1/2] = ( _Old ` _om ) with typecode |-