Theorem tposres

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

	Ref	Expression
Assertion	tposres	⊢ ( Rel 𝑅 → ( tpos 𝐹 ↾ 𝑅 ) = tpos ( 𝐹 ↾ ◡ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		0nelrel0	⊢ ( Rel 𝑅 → ¬ ∅ ∈ 𝑅 )
2		nel2nelin	⊢ ( ¬ ∅ ∈ 𝑅 → ¬ ∅ ∈ ( dom 𝐹 ∩ 𝑅 ) )
3	1 2	syl	⊢ ( Rel 𝑅 → ¬ ∅ ∈ ( dom 𝐹 ∩ 𝑅 ) )
4	3	tposres3	⊢ ( Rel 𝑅 → ( tpos 𝐹 ↾ 𝑅 ) = tpos ( 𝐹 ↾ ◡ 𝑅 ) )