Theorem elz12s

Description: Membership in the dyadic fractions. (Contributed by Scott Fenton, 7-Aug-2025)

	Ref	Expression
Assertion	elz12s	⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ ℤs[1/2] → 𝐴 ∈ V )
2		id	⊢ ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
3		ovex	⊢ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ∈ V
4	2 3	eqeltrdi	⊢ ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → 𝐴 ∈ V )
5	4	a1i	⊢ ( ( 𝑥 ∈ ℤs ∧ 𝑦 ∈ ℕ0s ) → ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → 𝐴 ∈ V ) )
6	5	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → 𝐴 ∈ V )
7		eqeq1	⊢ ( 𝑧 = 𝐴 → ( 𝑧 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ↔ 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) )
8	7	2rexbidv	⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝑧 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) )
9		df-z12s	⊢ ℤs[1/2] = { 𝑧 ∣ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝑧 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) }
10	8 9	elab2g	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) )
11	1 6 10	pm5.21nii	⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )