Theorem relexp2

Description: A set operated on by the relation exponent to the second power is equal to the composition of the set with itself. (Contributed by RP, 1-Jun-2020)

	Ref	Expression
Assertion	relexp2	$$⊢R\in V\to R{\uparrow }_{r}2=R\circ R$$

Proof

Step	Hyp	Ref	Expression
1		df-2	$$⊢2=1+1$$
2	1	oveq2i	$$⊢R{\uparrow }_{r}2=R{\uparrow }_r\left(1+1\right)$$
3	2	a1i	$$⊢R\in V\to R{\uparrow }_{r}2=R{\uparrow }_r\left(1+1\right)$$
4		1nn	$$⊢1\in \mathbb{N}$$
5		relexpsucnnr	$$⊢\left(R\in V\wedge 1\in \mathbb{N}\right)\to R{\uparrow }_r\left(1+1\right)=\left(R{\uparrow }_{r}1\right)\circ R$$
6	4 5	mpan2	$$⊢R\in V\to R{\uparrow }_r\left(1+1\right)=\left(R{\uparrow }_{r}1\right)\circ R$$
7		relexp1g	$$⊢R\in V\to R{\uparrow }_{r}1=R$$
8	7	coeq1d	$$⊢R\in V\to \left(R{\uparrow }_{r}1\right)\circ R=R\circ R$$
9	3 6 8	3eqtrd	$$⊢R\in V\to R{\uparrow }_{r}2=R\circ R$$