Theorem tposidres

Description: Swap an ordered pair. (Contributed by Zhi Wang, 5-Oct-2025)

	Ref	Expression
Hypotheses	tposidres.x	|- ( ph -> X e. A )
	tposidres.y	|- ( ph -> Y e. B )
Assertion	tposidres	|- ( ph -> ( Y tpos ( _I |` ( A X. B ) ) X ) = <. X , Y >. )

Proof

Step	Hyp	Ref	Expression
1		tposidres.x	|- ( ph -> X e. A )
2		tposidres.y	|- ( ph -> Y e. B )
3		ovtpos	|- ( Y tpos ( _I |` ( A X. B ) ) X ) = ( X ( _I |` ( A X. B ) ) Y )
4		df-ov	|- ( X ( _I |` ( A X. B ) ) Y ) = ( ( _I |` ( A X. B ) ) ` <. X , Y >. )
5	3 4	eqtri	|- ( Y tpos ( _I |` ( A X. B ) ) X ) = ( ( _I |` ( A X. B ) ) ` <. X , Y >. )
6	1 2	opelxpd	|- ( ph -> <. X , Y >. e. ( A X. B ) )
7	6	fvresd	|- ( ph -> ( ( _I |` ( A X. B ) ) ` <. X , Y >. ) = ( _I ` <. X , Y >. ) )
8	5 7	eqtrid	|- ( ph -> ( Y tpos ( _I |` ( A X. B ) ) X ) = ( _I ` <. X , Y >. ) )
9		opex	|- <. X , Y >. e. _V
10		fvi	|- ( <. X , Y >. e. _V -> ( _I ` <. X , Y >. ) = <. X , Y >. )
11	9 10	ax-mp	|- ( _I ` <. X , Y >. ) = <. X , Y >.
12	8 11	eqtrdi	|- ( ph -> ( Y tpos ( _I |` ( A X. B ) ) X ) = <. X , Y >. )