Theorem relexpcnvd

Description: Commutation of converse and relation exponentiation. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypotheses	relexpcnvd.1	$$⊢\phi \to R\in V$$
	relexpcnvd.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	relexpcnvd	$$⊢\phi \to {\left(R{\uparrow }_{r}N\right)}^{-1}=R^{-1}{\uparrow }_{r}N$$

Proof

Step	Hyp	Ref	Expression
1		relexpcnvd.1	$$⊢\phi \to R\in V$$
2		relexpcnvd.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
3		relexpcnv	$$⊢\left(N\in {\mathbb{N}}_0\wedge R\in V\right)\to {\left(R{\uparrow }_{r}N\right)}^{-1}=R^{-1}{\uparrow }_{r}N$$
4	2 1 3	syl2anc	$$⊢\phi \to {\left(R{\uparrow }_{r}N\right)}^{-1}=R^{-1}{\uparrow }_{r}N$$