Theorem pzriprnglem3

Description: Lemma 3 for pzriprng : An element of I is an ordered pair. (Contributed by AV, 18-Mar-2025)

	Ref	Expression
Hypotheses	pzriprng.r	⊢ 𝑅 = ( ℤring ×s ℤring )
	pzriprng.i	⊢ 𝐼 = ( ℤ × { 0 } )
Assertion	pzriprnglem3	⊢ ( 𝑋 ∈ 𝐼 ↔ ∃ 𝑥 ∈ ℤ 𝑋 = ⟨ 𝑥 , 0 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	⊢ 𝑅 = ( ℤring ×s ℤring )
2		pzriprng.i	⊢ 𝐼 = ( ℤ × { 0 } )
3	2	eleq2i	⊢ ( 𝑋 ∈ 𝐼 ↔ 𝑋 ∈ ( ℤ × { 0 } ) )
4		elxp2	⊢ ( 𝑋 ∈ ( ℤ × { 0 } ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ { 0 } 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ )
5		0z	⊢ 0 ∈ ℤ
6		opeq2	⊢ ( 𝑦 = 0 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 0 ⟩ )
7	6	eqeq2d	⊢ ( 𝑦 = 0 → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 𝑥 , 0 ⟩ ) )
8	7	rexsng	⊢ ( 0 ∈ ℤ → ( ∃ 𝑦 ∈ { 0 } 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 𝑥 , 0 ⟩ ) )
9	5 8	ax-mp	⊢ ( ∃ 𝑦 ∈ { 0 } 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 𝑥 , 0 ⟩ )
10	9	rexbii	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ { 0 } 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑥 ∈ ℤ 𝑋 = ⟨ 𝑥 , 0 ⟩ )
11	3 4 10	3bitri	⊢ ( 𝑋 ∈ 𝐼 ↔ ∃ 𝑥 ∈ ℤ 𝑋 = ⟨ 𝑥 , 0 ⟩ )