Theorem tposideq2

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

	Ref	Expression
Hypothesis	tposideq2.1	|- R = ( A X. B )
Assertion	tposideq2	|- ( tpos _I |` R ) = ( x e. R |-> U. `' { x } )

Proof

Step	Hyp	Ref	Expression
1		tposideq2.1	|- R = ( A X. B )
2		relxp	|- Rel ( A X. B )
3	1	releqi	|- ( Rel R <-> Rel ( A X. B ) )
4	2 3	mpbir	|- Rel R
5		tposideq	|- ( Rel R -> ( tpos _I |` R ) = ( x e. R |-> U. `' { x } ) )
6	4 5	ax-mp	|- ( tpos _I |` R ) = ( x e. R |-> U. `' { x } )