Theorem relexp1idm

Description: Repeated raising a relation to the first power is idempotent. (Contributed by RP, 12-Jun-2020)

	Ref	Expression
Assertion	relexp1idm	$$⊢R\in V\to \left(R{\uparrow }_{r}1\right){\uparrow }_{r}1=R{\uparrow }_{r}1$$

Proof

Step	Hyp	Ref	Expression
1		ifid	$$⊢if\left(1<1,1,1\right)=1$$
2	1	eqcomi	$$⊢1=if\left(1<1,1,1\right)$$
3	2	jctr	$$⊢R\in V\to \left(R\in V\wedge 1=if\left(1<1,1,1\right)\right)$$
4		1ex	$$⊢1\in \mathrm{V}$$
5	4	prid2	$$⊢1\in \left\{0,1\right\}$$
6	5 5	pm3.2i	$$⊢\left(1\in \left\{0,1\right\}\wedge 1\in \left\{0,1\right\}\right)$$
7		relexp01min	$$⊢\left(\left(R\in V\wedge 1=if\left(1<1,1,1\right)\right)\wedge \left(1\in \left\{0,1\right\}\wedge 1\in \left\{0,1\right\}\right)\right)\to \left(R{\uparrow }_{r}1\right){\uparrow }_{r}1=R{\uparrow }_{r}1$$
8	3 6 7	sylancl	$$⊢R\in V\to \left(R{\uparrow }_{r}1\right){\uparrow }_{r}1=R{\uparrow }_{r}1$$