Theorem tposres

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

	Ref	Expression
Assertion	tposres	$$⊢\mathrm{Rel}R\to {tposF\upharpoonright }_R=tpos\left({F\upharpoonright }_{R^{-1}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		0nelrel0	$$⊢\mathrm{Rel}R\to \neg \varnothing \in R$$
2		nel2nelin	$$⊢\neg \varnothing \in R\to \neg \varnothing \in \left(\mathrm{dom}F\cap R\right)$$
3	1 2	syl	$$⊢\mathrm{Rel}R\to \neg \varnothing \in \left(\mathrm{dom}F\cap R\right)$$
4	3	tposres3	$$⊢\mathrm{Rel}R\to {tposF\upharpoonright }_R=tpos\left({F\upharpoonright }_{R^{-1}}\right)$$