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 r N = I A

Proof

Step Hyp Ref Expression
1 oveq2 x = 0 I A r x = I A r 0
2 1 eqeq1d x = 0 I A r x = I A I A r 0 = I A
3 2 imbi2d x = 0 A V I A r x = I A A V I A r 0 = I A
4 oveq2 x = y I A r x = I A r y
5 4 eqeq1d x = y I A r x = I A I A r y = I A
6 5 imbi2d x = y A V I A r x = I A A V I A r y = I A
7 oveq2 x = y + 1 I A r x = I A r y + 1
8 7 eqeq1d x = y + 1 I A r x = I A I A r y + 1 = I A
9 8 imbi2d x = y + 1 A V I A r x = I A A V I A r y + 1 = I A
10 oveq2 x = N I A r x = I A r N
11 10 eqeq1d x = N I A r x = I A I A r N = I A
12 11 imbi2d x = N A V I A r x = I A A V I A r N = I A
13 resiexg A V I A V
14 relexp0g I A V I A r 0 = I dom I A ran I A
15 13 14 syl A V I A r 0 = 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 syl6eq A V I A r 0 = I A
23 relres Rel I A
24 23 a1i I A r y = I A A V Rel I A
25 13 adantl I A r y = I A A V I A V
26 24 25 relexpsucrd I A r y = I A A V y 0 I A r y + 1 = I A r y I A
27 26 3impia I A r y = I A A V y 0 I A r y + 1 = I A r y I A
28 simp1 I A r y = I A A V y 0 I A r y = I A
29 28 coeq1d I A r y = I A A V y 0 I A r y I A = I A I A
30 coires1 I A I A = I A A
31 residm I A A = I A
32 30 31 eqtri I A I A = I A
33 29 32 syl6eq I A r y = I A A V y 0 I A r y I A = I A
34 27 33 eqtrd I A r y = I A A V y 0 I A r y + 1 = I A
35 34 3exp I A r y = I A A V y 0 I A r y + 1 = I A
36 35 com13 y 0 A V I A r y = I A I A r y + 1 = I A
37 36 a2d y 0 A V I A r y = I A A V I A r y + 1 = I A
38 3 6 9 12 22 37 nn0ind N 0 A V I A r N = I A
39 38 impcom A V N 0 I A r N = I A