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	$$⊢R={\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}$$
	pzriprng.i	$$⊢I=\mathbb{Z}\times \left\{0\right\}$$
Assertion	pzriprnglem3	$$⊢X\in I\leftrightarrow \exists x\in \mathbb{Z}X=⟨x,0⟩$$

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	$$⊢R={\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}$$
2		pzriprng.i	$$⊢I=\mathbb{Z}\times \left\{0\right\}$$
3	2	eleq2i	$$⊢X\in I\leftrightarrow X\in \left(\mathbb{Z}\times \left\{0\right\}\right)$$
4		elxp2	$$⊢X\in \left(\mathbb{Z}\times \left\{0\right\}\right)\leftrightarrow \exists x\in \mathbb{Z}\exists y\in \left\{0\right\}X=⟨x,y⟩$$
5		0z	$$⊢0\in \mathbb{Z}$$
6		opeq2	$$⊢y=0\to ⟨x,y⟩=⟨x,0⟩$$
7	6	eqeq2d	$$⊢y=0\to \left(X=⟨x,y⟩\leftrightarrow X=⟨x,0⟩\right)$$
8	7	rexsng	$$⊢0\in \mathbb{Z}\to \left(\exists y\in \left\{0\right\}X=⟨x,y⟩\leftrightarrow X=⟨x,0⟩\right)$$
9	5 8	ax-mp	$$⊢\exists y\in \left\{0\right\}X=⟨x,y⟩\leftrightarrow X=⟨x,0⟩$$
10	9	rexbii	$$⊢\exists x\in \mathbb{Z}\exists y\in \left\{0\right\}X=⟨x,y⟩\leftrightarrow \exists x\in \mathbb{Z}X=⟨x,0⟩$$
11	3 4 10	3bitri	$$⊢X\in I\leftrightarrow \exists x\in \mathbb{Z}X=⟨x,0⟩$$