Theorem tposid

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

	Ref	Expression
Assertion	tposid	⊢ ( 𝑋 tpos I 𝑌 ) = ⟨ 𝑌 , 𝑋 ⟩

Proof

Step	Hyp	Ref	Expression
1		ovtpos	⊢ ( 𝑋 tpos I 𝑌 ) = ( 𝑌 I 𝑋 )
2		df-ov	⊢ ( 𝑌 I 𝑋 ) = ( I ‘ ⟨ 𝑌 , 𝑋 ⟩ )
3		opex	⊢ ⟨ 𝑌 , 𝑋 ⟩ ∈ V
4		fvi	⊢ ( ⟨ 𝑌 , 𝑋 ⟩ ∈ V → ( I ‘ ⟨ 𝑌 , 𝑋 ⟩ ) = ⟨ 𝑌 , 𝑋 ⟩ )
5	3 4	ax-mp	⊢ ( I ‘ ⟨ 𝑌 , 𝑋 ⟩ ) = ⟨ 𝑌 , 𝑋 ⟩
6	1 2 5	3eqtri	⊢ ( 𝑋 tpos I 𝑌 ) = ⟨ 𝑌 , 𝑋 ⟩