Metamath Proof Explorer

Definition df-relexp

Description: Definition of repeated composition of a relation with itself, aka relation exponentiation. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 22-May-2020)

Ref Expression
Assertion df-relexp ⊢ ↑ r = r ∈ V , n ∈ ℕ 0 ⟼ if n = 0 I ↾ dom ⁡ r ∪ ran ⁡ r seq 1 x ∈ V , y ∈ V ⟼ x ∘ r z ∈ V ⟼ r ⁡ n

Detailed syntax breakdown

Step Hyp Ref Expression
0 crelexp class ↑ r
1 vr setvar r
2 cvv class V
3 vn setvar n
4 cn0 class ℕ 0
5 3 cv setvar n
6 cc0 class 0
7 5 6 wceq wff n = 0
8 cid class I
9 1 cv setvar r
10 9 cdm class dom ⁡ r
11 9 crn class ran ⁡ r
12 10 11 cun class dom ⁡ r ∪ ran ⁡ r
13 8 12 cres class I ↾ dom ⁡ r ∪ ran ⁡ r
14 c1 class 1
15 vx setvar x
16 vy setvar y
17 15 cv setvar x
18 17 9 ccom class x ∘ r
19 15 16 2 2 18 cmpo class x ∈ V , y ∈ V ⟼ x ∘ r
20 vz setvar z
21 20 2 9 cmpt class z ∈ V ⟼ r
22 19 21 14 cseq class seq 1 x ∈ V , y ∈ V ⟼ x ∘ r z ∈ V ⟼ r
23 5 22 cfv class seq 1 x ∈ V , y ∈ V ⟼ x ∘ r z ∈ V ⟼ r ⁡ n
24 7 13 23 cif class if n = 0 I ↾ dom ⁡ r ∪ ran ⁡ r seq 1 x ∈ V , y ∈ V ⟼ x ∘ r z ∈ V ⟼ r ⁡ n
25 1 3 2 4 24 cmpo class r ∈ V , n ∈ ℕ 0 ⟼ if n = 0 I ↾ dom ⁡ r ∪ ran ⁡ r seq 1 x ∈ V , y ∈ V ⟼ x ∘ r z ∈ V ⟼ r ⁡ n
26 0 25 wceq wff ↑ r = r ∈ V , n ∈ ℕ 0 ⟼ if n = 0 I ↾ dom ⁡ r ∪ ran ⁡ r seq 1 x ∈ V , y ∈ V ⟼ x ∘ r z ∈ V ⟼ r ⁡ n