Theorem tposid

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

	Ref	Expression
Assertion	tposid	|- ( X tpos _I Y ) = <. Y , X >.

Proof

Step	Hyp	Ref	Expression
1		ovtpos	|- ( X tpos _I Y ) = ( Y _I X )
2		df-ov	|- ( Y _I X ) = ( _I ` <. Y , X >. )
3		opex	|- <. Y , X >. e. _V
4		fvi	|- ( <. Y , X >. e. _V -> ( _I ` <. Y , X >. ) = <. Y , X >. )
5	3 4	ax-mp	|- ( _I ` <. Y , X >. ) = <. Y , X >.
6	1 2 5	3eqtri	|- ( X tpos _I Y ) = <. Y , X >.