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	⊢ ↑𝑟 = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crelexp	⊢ ↑𝑟
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vn	⊢ 𝑛
4		cn0	⊢ ℕ0
5	3	cv	⊢ 𝑛
6		cc0	⊢ 0
7	5 6	wceq	⊢ 𝑛 = 0
8		cid	⊢ I
9	1	cv	⊢ 𝑟
10	9	cdm	⊢ dom 𝑟
11	9	crn	⊢ ran 𝑟
12	10 11	cun	⊢ ( dom 𝑟 ∪ ran 𝑟 )
13	8 12	cres	⊢ ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) )
14		c1	⊢ 1
15		vx	⊢ 𝑥
16		vy	⊢ 𝑦
17	15	cv	⊢ 𝑥
18	17 9	ccom	⊢ ( 𝑥 ∘ 𝑟 )
19	15 16 2 2 18	cmpo	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) )
20		vz	⊢ 𝑧
21	20 2 9	cmpt	⊢ ( 𝑧 ∈ V ↦ 𝑟 )
22	19 21 14	cseq	⊢ seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) )
23	5 22	cfv	⊢ ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 )
24	7 13 23	cif	⊢ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) )
25	1 3 2 4 24	cmpo	⊢ ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) )
26	0 25	wceq	⊢ ↑𝑟 = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) )