Theorem tposres2

Description: The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Hypothesis	tposres2.1	|- ( ph -> -. (/) e. ( dom F i^i R ) )
Assertion	tposres2	|- ( ph -> ( tpos F |` R ) = ( tpos F |` `' `' R ) )

Proof

Step	Hyp	Ref	Expression
1		tposres2.1	|- ( ph -> -. (/) e. ( dom F i^i R ) )
2		tposresg	|- ( tpos F |` R ) = ( ( tpos F |` `' `' R ) u. ( F |` ( R i^i { (/) } ) ) )
3		resinsn	|- ( ( F |` ( R i^i { (/) } ) ) = (/) <-> -. (/) e. ( dom F i^i R ) )
4	1 3	sylibr	|- ( ph -> ( F |` ( R i^i { (/) } ) ) = (/) )
5	4	uneq2d	|- ( ph -> ( ( tpos F |` `' `' R ) u. ( F |` ( R i^i { (/) } ) ) ) = ( ( tpos F |` `' `' R ) u. (/) ) )
6	2 5	eqtrid	|- ( ph -> ( tpos F |` R ) = ( ( tpos F |` `' `' R ) u. (/) ) )
7		un0	|- ( ( tpos F |` `' `' R ) u. (/) ) = ( tpos F |` `' `' R )
8	6 7	eqtrdi	|- ( ph -> ( tpos F |` R ) = ( tpos F |` `' `' R ) )