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

Proof

Step	Hyp	Ref	Expression
1		zs12no	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		oldssno	$$⊢\mathrm{Old}\left(\mathrm{\omega }\right)\subseteq \mathrm{No}$$
3	2	sseli	$$⊢x\in \mathrm{Old}\left(\mathrm{\omega }\right)\to x\in \mathrm{No}$$
4		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 |-
5		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
6		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)$$
7	5 6	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)$$
8	4 7	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 |-
9	1 3 8	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 |-
10	9	eqriv	Could not format ZZ_s[1/2] = ( _Old ` _om ) : No typesetting found for |- ZZ_s[1/2] = ( _Old ` _om ) with typecode |-