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 eqtrdi ⊢ A ∈ V → I ↾ A ↑ r 0 = I ↾ A
23 relres ⊢ Rel ⁡ I ↾ A
24 23 a1i ⊢ I ↾ A ↑ r y = I ↾ A ∧ A ∈ V ∧ y ∈ ℕ 0 → Rel ⁡ I ↾ A
25 simp3 ⊢ I ↾ A ↑ r y = I ↾ A ∧ A ∈ V ∧ y ∈ ℕ 0 → y ∈ ℕ 0
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 simp1 ⊢ I ↾ A ↑ r y = I ↾ A ∧ A ∈ V ∧ y ∈ ℕ 0 → I ↾ A ↑ r y = I ↾ A
28 27 coeq1d ⊢ I ↾ A ↑ r y = I ↾ A ∧ A ∈ V ∧ y ∈ ℕ 0 → I ↾ A ↑ r y ∘ 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 ↑ r y = I ↾ A ∧ A ∈ V ∧ y ∈ ℕ 0 → I ↾ A ↑ r y ∘ I ↾ A = I ↾ A
33 26 32 eqtrd ⊢ I ↾ A ↑ r y = I ↾ A ∧ A ∈ V ∧ y ∈ ℕ 0 → I ↾ A ↑ r y + 1 = I ↾ A
34 33 3exp ⊢ I ↾ A ↑ r y = I ↾ A → A ∈ V → y ∈ ℕ 0 → I ↾ A ↑ r y + 1 = I ↾ A
35 34 com13 ⊢ y ∈ ℕ 0 → A ∈ V → I ↾ A ↑ r y = I ↾ A → I ↾ A ↑ r y + 1 = I ↾ A
36 35 a2d ⊢ y ∈ ℕ 0 → A ∈ V → I ↾ A ↑ r y = I ↾ A → A ∈ V → I ↾ A ↑ r y + 1 = I ↾ A
37 3 6 9 12 22 36 nn0ind ⊢ N ∈ ℕ 0 → A ∈ V → I ↾ A ↑ r N = I ↾ A
38 37 impcom ⊢ A ∈ V ∧ N ∈ ℕ 0 → I ↾ A ↑ r N = I ↾ A