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

Proof

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