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 ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( I ↾ 𝐴 ) ↑𝑟 𝑁 ) = ( I ↾ 𝐴 ) )

Proof

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