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 = ( ZZring Xs. ZZring )
	pzriprng.i	|- I = ( ZZ X. { 0 } )
Assertion	pzriprnglem3	|- ( X e. I <-> E. x e. ZZ X = <. x , 0 >. )

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	|- R = ( ZZring Xs. ZZring )
2		pzriprng.i	|- I = ( ZZ X. { 0 } )
3	2	eleq2i	|- ( X e. I <-> X e. ( ZZ X. { 0 } ) )
4		elxp2	|- ( X e. ( ZZ X. { 0 } ) <-> E. x e. ZZ E. y e. { 0 } X = <. x , y >. )
5		0z	|- 0 e. ZZ
6		opeq2	|- ( y = 0 -> <. x , y >. = <. x , 0 >. )
7	6	eqeq2d	|- ( y = 0 -> ( X = <. x , y >. <-> X = <. x , 0 >. ) )
8	7	rexsng	|- ( 0 e. ZZ -> ( E. y e. { 0 } X = <. x , y >. <-> X = <. x , 0 >. ) )
9	5 8	ax-mp	|- ( E. y e. { 0 } X = <. x , y >. <-> X = <. x , 0 >. )
10	9	rexbii	|- ( E. x e. ZZ E. y e. { 0 } X = <. x , y >. <-> E. x e. ZZ X = <. x , 0 >. )
11	3 4 10	3bitri	|- ( X e. I <-> E. x e. ZZ X = <. x , 0 >. )