Definition df-relexp 15153

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.)

Assertion

Ref	Expression
df-relexp	⊢ ↑𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))

Distinct variable group:   𝑛,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-relexp

Step	Hyp	Ref	Expression
1		crelexp 15152	. 2 class ↑𝑟
2		vr	. . 3 setvar 𝑟
3		vn	. . 3 setvar 𝑛
4		cvv 3451	. . 3 class V
5		cn0 12587	. . 3 class ℕ0
6	3	cv 1569	. . . . 5 class 𝑛
7		cc0 11181	. . . . 5 class 0
8	6, 7	wceq 1570	. . . 4 wff 𝑛 = 0
9		cid 5545	. . . . 5 class I
10	2	cv 1569	. . . . . . 7 class 𝑟
11	10	cdm 5651	. . . . . 6 class dom 𝑟
12	10	crn 5652	. . . . . 6 class ran 𝑟
13	11, 12	cun 3897	. . . . 5 class (dom 𝑟 ∪ ran 𝑟)
14	9, 13	cres 5653	. . . 4 class ( I ↾ (dom 𝑟 ∪ ran 𝑟))
15		vx	. . . . . . 7 setvar 𝑥
16		vy	. . . . . . 7 setvar 𝑦
17	15	cv 1569	. . . . . . . 8 class 𝑥
18	17, 10	ccom 5655	. . . . . . 7 class (𝑥 ∘ 𝑟)
19	15, 16, 4, 4, 18	cmpo 7414	. . . . . 6 class (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟))
20		vz	. . . . . . 7 setvar 𝑧
21	20, 4, 10	cmpt 5186	. . . . . 6 class (𝑧 ∈ V ↦ 𝑟)
22		c1 11182	. . . . . 6 class 1
23	19, 21, 22	cseq 14124	. . . . 5 class seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))
24	6, 23	cfv 6531	. . . 4 class (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)
25	8, 14, 24	cif 4482	. . 3 class if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛))
26	2, 3, 4, 5, 25	cmpo 7414	. 2 class (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))
27	1, 26	wceq 1570	1 wff ↑𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))

This definition is used by:  reldmrelexp  15154  relexp0g  15155  relexpsucnnr  15158  relexp1g  15159