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 ⊢A∈V∧N∈ℕ0→I↾A↑rN=I↾A

Proof

Step Hyp Ref Expression
1 oveq2 ⊢x=0→I↾A↑rx=I↾A↑r0
2 1 eqeq1d ⊢x=0→I↾A↑rx=I↾A↔I↾A↑r0=I↾A
3 2 imbi2d ⊢x=0→A∈V→I↾A↑rx=I↾A↔A∈V→I↾A↑r0=I↾A
4 oveq2 ⊢x=y→I↾A↑rx=I↾A↑ry
5 4 eqeq1d ⊢x=y→I↾A↑rx=I↾A↔I↾A↑ry=I↾A
6 5 imbi2d ⊢x=y→A∈V→I↾A↑rx=I↾A↔A∈V→I↾A↑ry=I↾A
7 oveq2 ⊢x=y+1→I↾A↑rx=I↾A↑ry+1
8 7 eqeq1d ⊢x=y+1→I↾A↑rx=I↾A↔I↾A↑ry+1=I↾A
9 8 imbi2d ⊢x=y+1→A∈V→I↾A↑rx=I↾A↔A∈V→I↾A↑ry+1=I↾A
10 oveq2 ⊢x=N→I↾A↑rx=I↾A↑rN
11 10 eqeq1d ⊢x=N→I↾A↑rx=I↾A↔I↾A↑rN=I↾A
12 11 imbi2d ⊢x=N→A∈V→I↾A↑rx=I↾A↔A∈V→I↾A↑rN=I↾A
13 resiexg ⊢A∈V→I↾A∈V
14 relexp0g ⊢I↾A∈V→I↾A↑r0=I↾dom⁡I↾A∪ran⁡I↾A
15 13 14 syl ⊢A∈V→I↾A↑r0=I↾dom⁡I↾A∪ran⁡I↾A
16 dmresi ⊢dom⁡I↾A=A
17 rnresi ⊢ran⁡I↾A=A
18 16 17 uneq12i ⊢dom⁡I↾A∪ran⁡I↾A=A∪A
19 unidm ⊢A∪A=A
20 18 19 eqtri ⊢dom⁡I↾A∪ran⁡I↾A=A
21 20 reseq2i ⊢I↾dom⁡I↾A∪ran⁡I↾A=I↾A
22 15 21 eqtrdi ⊢A∈V→I↾A↑r0=I↾A
23 relres ⊢Rel⁡I↾A
24 23 a1i ⊢I↾A↑ry=I↾A∧A∈V∧y∈ℕ0→Rel⁡I↾A
25 simp3 ⊢I↾A↑ry=I↾A∧A∈V∧y∈ℕ0→y∈ℕ0
26 24 25 relexpsucrd ⊢I↾A↑ry=I↾A∧A∈V∧y∈ℕ0→I↾A↑ry+1=I↾A↑ry∘I↾A
27 simp1 ⊢I↾A↑ry=I↾A∧A∈V∧y∈ℕ0→I↾A↑ry=I↾A
28 27 coeq1d ⊢I↾A↑ry=I↾A∧A∈V∧y∈ℕ0→I↾A↑ry∘I↾A=I↾A∘I↾A
29 coires1 ⊢I↾A∘I↾A=I↾A↾A
30 residm ⊢I↾A↾A=I↾A
31 29 30 eqtri ⊢I↾A∘I↾A=I↾A
32 28 31 eqtrdi ⊢I↾A↑ry=I↾A∧A∈V∧y∈ℕ0→I↾A↑ry∘I↾A=I↾A
33 26 32 eqtrd ⊢I↾A↑ry=I↾A∧A∈V∧y∈ℕ0→I↾A↑ry+1=I↾A
34 33 3exp ⊢I↾A↑ry=I↾A→A∈V→y∈ℕ0→I↾A↑ry+1=I↾A
35 34 com13 ⊢y∈ℕ0→A∈V→I↾A↑ry=I↾A→I↾A↑ry+1=I↾A
36 35 a2d ⊢y∈ℕ0→A∈V→I↾A↑ry=I↾A→A∈V→I↾A↑ry+1=I↾A
37 3 6 9 12 22 36 nn0ind ⊢N∈ℕ0→A∈V→I↾A↑rN=I↾A
38 37 impcom ⊢A∈V∧N∈ℕ0→I↾A↑rN=I↾A