Theorem tposidres

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

	Ref	Expression
Hypotheses	tposidres.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	tposidres.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	tposidres	⊢ ( 𝜑 → ( 𝑌 tpos ( I ↾ ( 𝐴 × 𝐵 ) ) 𝑋 ) = ⟨ 𝑋 , 𝑌 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		tposidres.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
2		tposidres.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
3		ovtpos	⊢ ( 𝑌 tpos ( I ↾ ( 𝐴 × 𝐵 ) ) 𝑋 ) = ( 𝑋 ( I ↾ ( 𝐴 × 𝐵 ) ) 𝑌 )
4		df-ov	⊢ ( 𝑋 ( I ↾ ( 𝐴 × 𝐵 ) ) 𝑌 ) = ( ( I ↾ ( 𝐴 × 𝐵 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
5	3 4	eqtri	⊢ ( 𝑌 tpos ( I ↾ ( 𝐴 × 𝐵 ) ) 𝑋 ) = ( ( I ↾ ( 𝐴 × 𝐵 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
6	1 2	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × 𝐵 ) )
7	6	fvresd	⊢ ( 𝜑 → ( ( I ↾ ( 𝐴 × 𝐵 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( I ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
8	5 7	eqtrid	⊢ ( 𝜑 → ( 𝑌 tpos ( I ↾ ( 𝐴 × 𝐵 ) ) 𝑋 ) = ( I ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
9		opex	⊢ ⟨ 𝑋 , 𝑌 ⟩ ∈ V
10		fvi	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ V → ( I ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ 𝑋 , 𝑌 ⟩ )
11	9 10	ax-mp	⊢ ( I ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ 𝑋 , 𝑌 ⟩
12	8 11	eqtrdi	⊢ ( 𝜑 → ( 𝑌 tpos ( I ↾ ( 𝐴 × 𝐵 ) ) 𝑋 ) = ⟨ 𝑋 , 𝑌 ⟩ )