Theorem tposideq2

Description: Two ways of expressing the swap function. (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Hypothesis	tposideq2.1	⊢ 𝑅 = ( 𝐴 × 𝐵 )
Assertion	tposideq2	⊢ ( tpos I ↾ 𝑅 ) = ( 𝑥 ∈ 𝑅 ↦ ∪ ◡ { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		tposideq2.1	⊢ 𝑅 = ( 𝐴 × 𝐵 )
2		relxp	⊢ Rel ( 𝐴 × 𝐵 )
3	1	releqi	⊢ ( Rel 𝑅 ↔ Rel ( 𝐴 × 𝐵 ) )
4	2 3	mpbir	⊢ Rel 𝑅
5		tposideq	⊢ ( Rel 𝑅 → ( tpos I ↾ 𝑅 ) = ( 𝑥 ∈ 𝑅 ↦ ∪ ◡ { 𝑥 } ) )
6	4 5	ax-mp	⊢ ( tpos I ↾ 𝑅 ) = ( 𝑥 ∈ 𝑅 ↦ ∪ ◡ { 𝑥 } )