# Metamath Proof Explorer

## Theorem relexpiidm

Description: Any power of any restriction of the identity relation is itself. (Contributed by RP, 12-Jun-2020)

Ref Expression
Assertion relexpiidm ${⊢}\left({A}\in {V}\wedge {N}\in {ℕ}_{0}\right)\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{N}={\mathrm{I}↾}_{{A}}$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{x}=0\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}=\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}0$
2 1 eqeq1d ${⊢}{x}=0\to \left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}={\mathrm{I}↾}_{{A}}↔\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}0={\mathrm{I}↾}_{{A}}\right)$
3 2 imbi2d ${⊢}{x}=0\to \left(\left({A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}={\mathrm{I}↾}_{{A}}\right)↔\left({A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}0={\mathrm{I}↾}_{{A}}\right)\right)$
4 oveq2 ${⊢}{x}={y}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}=\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}$
5 4 eqeq1d ${⊢}{x}={y}\to \left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}={\mathrm{I}↾}_{{A}}↔\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\right)$
6 5 imbi2d ${⊢}{x}={y}\to \left(\left({A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}={\mathrm{I}↾}_{{A}}\right)↔\left({A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\right)\right)$
7 oveq2 ${⊢}{x}={y}+1\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}=\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}\left({y}+1\right)$
8 7 eqeq1d ${⊢}{x}={y}+1\to \left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}={\mathrm{I}↾}_{{A}}↔\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}\left({y}+1\right)={\mathrm{I}↾}_{{A}}\right)$
9 8 imbi2d ${⊢}{x}={y}+1\to \left(\left({A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}={\mathrm{I}↾}_{{A}}\right)↔\left({A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}\left({y}+1\right)={\mathrm{I}↾}_{{A}}\right)\right)$
10 oveq2 ${⊢}{x}={N}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}=\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{N}$
11 10 eqeq1d ${⊢}{x}={N}\to \left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}={\mathrm{I}↾}_{{A}}↔\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{N}={\mathrm{I}↾}_{{A}}\right)$
12 11 imbi2d ${⊢}{x}={N}\to \left(\left({A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{x}={\mathrm{I}↾}_{{A}}\right)↔\left({A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{N}={\mathrm{I}↾}_{{A}}\right)\right)$
13 resiexg ${⊢}{A}\in {V}\to {\mathrm{I}↾}_{{A}}\in \mathrm{V}$
14 relexp0g ${⊢}{\mathrm{I}↾}_{{A}}\in \mathrm{V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}0={\mathrm{I}↾}_{\left(\mathrm{dom}\left({\mathrm{I}↾}_{{A}}\right)\cup \mathrm{ran}\left({\mathrm{I}↾}_{{A}}\right)\right)}$
15 13 14 syl ${⊢}{A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}0={\mathrm{I}↾}_{\left(\mathrm{dom}\left({\mathrm{I}↾}_{{A}}\right)\cup \mathrm{ran}\left({\mathrm{I}↾}_{{A}}\right)\right)}$
16 dmresi ${⊢}\mathrm{dom}\left({\mathrm{I}↾}_{{A}}\right)={A}$
17 rnresi ${⊢}\mathrm{ran}\left({\mathrm{I}↾}_{{A}}\right)={A}$
18 16 17 uneq12i ${⊢}\mathrm{dom}\left({\mathrm{I}↾}_{{A}}\right)\cup \mathrm{ran}\left({\mathrm{I}↾}_{{A}}\right)={A}\cup {A}$
19 unidm ${⊢}{A}\cup {A}={A}$
20 18 19 eqtri ${⊢}\mathrm{dom}\left({\mathrm{I}↾}_{{A}}\right)\cup \mathrm{ran}\left({\mathrm{I}↾}_{{A}}\right)={A}$
21 20 reseq2i ${⊢}{\mathrm{I}↾}_{\left(\mathrm{dom}\left({\mathrm{I}↾}_{{A}}\right)\cup \mathrm{ran}\left({\mathrm{I}↾}_{{A}}\right)\right)}={\mathrm{I}↾}_{{A}}$
22 15 21 syl6eq ${⊢}{A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}0={\mathrm{I}↾}_{{A}}$
23 relres ${⊢}\mathrm{Rel}\left({\mathrm{I}↾}_{{A}}\right)$
24 23 a1i ${⊢}\left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\wedge {A}\in {V}\right)\to \mathrm{Rel}\left({\mathrm{I}↾}_{{A}}\right)$
25 13 adantl ${⊢}\left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\wedge {A}\in {V}\right)\to {\mathrm{I}↾}_{{A}}\in \mathrm{V}$
26 24 25 relexpsucrd ${⊢}\left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\wedge {A}\in {V}\right)\to \left({y}\in {ℕ}_{0}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}\left({y}+1\right)=\left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}\right)\circ \left({\mathrm{I}↾}_{{A}}\right)\right)$
27 26 3impia ${⊢}\left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\wedge {A}\in {V}\wedge {y}\in {ℕ}_{0}\right)\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}\left({y}+1\right)=\left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}\right)\circ \left({\mathrm{I}↾}_{{A}}\right)$
28 simp1 ${⊢}\left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\wedge {A}\in {V}\wedge {y}\in {ℕ}_{0}\right)\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}$
29 28 coeq1d ${⊢}\left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\wedge {A}\in {V}\wedge {y}\in {ℕ}_{0}\right)\to \left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}\right)\circ \left({\mathrm{I}↾}_{{A}}\right)=\left({\mathrm{I}↾}_{{A}}\right)\circ \left({\mathrm{I}↾}_{{A}}\right)$
30 coires1 ${⊢}\left({\mathrm{I}↾}_{{A}}\right)\circ \left({\mathrm{I}↾}_{{A}}\right)={\left({\mathrm{I}↾}_{{A}}\right)↾}_{{A}}$
31 residm ${⊢}{\left({\mathrm{I}↾}_{{A}}\right)↾}_{{A}}={\mathrm{I}↾}_{{A}}$
32 30 31 eqtri ${⊢}\left({\mathrm{I}↾}_{{A}}\right)\circ \left({\mathrm{I}↾}_{{A}}\right)={\mathrm{I}↾}_{{A}}$
33 29 32 syl6eq ${⊢}\left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\wedge {A}\in {V}\wedge {y}\in {ℕ}_{0}\right)\to \left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}\right)\circ \left({\mathrm{I}↾}_{{A}}\right)={\mathrm{I}↾}_{{A}}$
34 27 33 eqtrd ${⊢}\left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\wedge {A}\in {V}\wedge {y}\in {ℕ}_{0}\right)\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}\left({y}+1\right)={\mathrm{I}↾}_{{A}}$
35 34 3exp ${⊢}\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\to \left({A}\in {V}\to \left({y}\in {ℕ}_{0}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}\left({y}+1\right)={\mathrm{I}↾}_{{A}}\right)\right)$
36 35 com13 ${⊢}{y}\in {ℕ}_{0}\to \left({A}\in {V}\to \left(\left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}\left({y}+1\right)={\mathrm{I}↾}_{{A}}\right)\right)$
37 36 a2d ${⊢}{y}\in {ℕ}_{0}\to \left(\left({A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{y}={\mathrm{I}↾}_{{A}}\right)\to \left({A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}\left({y}+1\right)={\mathrm{I}↾}_{{A}}\right)\right)$
38 3 6 9 12 22 37 nn0ind ${⊢}{N}\in {ℕ}_{0}\to \left({A}\in {V}\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{N}={\mathrm{I}↾}_{{A}}\right)$
39 38 impcom ${⊢}\left({A}\in {V}\wedge {N}\in {ℕ}_{0}\right)\to \left({\mathrm{I}↾}_{{A}}\right){↑}_{r}{N}={\mathrm{I}↾}_{{A}}$