Theorem relexp0idm

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

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

Proof

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