Theorem tposres2

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

	Ref	Expression
Hypothesis	tposres2.1	⊢ ( 𝜑 → ¬ ∅ ∈ ( dom 𝐹 ∩ 𝑅 ) )
Assertion	tposres2	⊢ ( 𝜑 → ( tpos 𝐹 ↾ 𝑅 ) = ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		tposres2.1	⊢ ( 𝜑 → ¬ ∅ ∈ ( dom 𝐹 ∩ 𝑅 ) )
2		tposresg	⊢ ( tpos 𝐹 ↾ 𝑅 ) = ( ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) ∪ ( 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) )
3		resinsn	⊢ ( ( 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) = ∅ ↔ ¬ ∅ ∈ ( dom 𝐹 ∩ 𝑅 ) )
4	1 3	sylibr	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) = ∅ )
5	4	uneq2d	⊢ ( 𝜑 → ( ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) ∪ ( 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) ) = ( ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) ∪ ∅ ) )
6	2 5	eqtrid	⊢ ( 𝜑 → ( tpos 𝐹 ↾ 𝑅 ) = ( ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) ∪ ∅ ) )
7		un0	⊢ ( ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) ∪ ∅ ) = ( tpos 𝐹 ↾ ◡ ◡ 𝑅 )
8	6 7	eqtrdi	⊢ ( 𝜑 → ( tpos 𝐹 ↾ 𝑅 ) = ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) )