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	⊢ ℤs[1/2] = ( O ‘ ω )

Proof

Step	Hyp	Ref	Expression
1		zs12no	⊢ ( 𝑥 ∈ ℤs[1/2] → 𝑥 ∈ No )
2		oldssno	⊢ ( O ‘ ω ) ⊆ No
3	2	sseli	⊢ ( 𝑥 ∈ ( O ‘ ω ) → 𝑥 ∈ No )
4		bdayfin	⊢ ( 𝑥 ∈ No → ( 𝑥 ∈ ℤs[1/2] ↔ ( bday ‘ 𝑥 ) ∈ ω ) )
5		omelon	⊢ ω ∈ On
6		oldbday	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ No ) → ( 𝑥 ∈ ( O ‘ ω ) ↔ ( bday ‘ 𝑥 ) ∈ ω ) )
7	5 6	mpan	⊢ ( 𝑥 ∈ No → ( 𝑥 ∈ ( O ‘ ω ) ↔ ( bday ‘ 𝑥 ) ∈ ω ) )
8	4 7	bitr4d	⊢ ( 𝑥 ∈ No → ( 𝑥 ∈ ℤs[1/2] ↔ 𝑥 ∈ ( O ‘ ω ) ) )
9	1 3 8	pm5.21nii	⊢ ( 𝑥 ∈ ℤs[1/2] ↔ 𝑥 ∈ ( O ‘ ω ) )
10	9	eqriv	⊢ ℤs[1/2] = ( O ‘ ω )