Theorem z12sex

Description: The class of dyadic fractions is a set. (Contributed by Scott Fenton, 7-Aug-2025)

	Ref	Expression
Assertion	z12sex	⊢ ℤs[1/2] ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-z12s	⊢ ℤs[1/2] = { 𝑥 ∣ ∃ 𝑦 ∈ ℤs ∃ 𝑧 ∈ ℕ0s 𝑥 = ( 𝑦 /su ( 2s ↑s 𝑧 ) ) }
2		zsex	⊢ ℤs ∈ V
3		n0sex	⊢ ℕ0s ∈ V
4	2 3	ab2rexex	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℤs ∃ 𝑧 ∈ ℕ0s 𝑥 = ( 𝑦 /su ( 2s ↑s 𝑧 ) ) } ∈ V
5	1 4	eqeltri	⊢ ℤs[1/2] ∈ V