Definition df-relexp 13761

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	|- ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) )

Distinct variable group:   n, r, x, y, z

Detailed syntax breakdown of Definition df-relexp

Step	Hyp	Ref	Expression
1		crelexp 13760	. 2 class ^r
2		vr	. . 3 setvar r
3		vn	. . 3 setvar n
4		cvv 3200	. . 3 class _V
5		cn0 11292	. . 3 class NN0
6	3	cv 1482	. . . . 5 class n
7		cc0 9936	. . . . 5 class 0
8	6, 7	wceq 1483	. . . 4 wff n = 0
9		cid 5023	. . . . 5 class _I
10	2	cv 1482	. . . . . . 7 class r
11	10	cdm 5114	. . . . . 6 class dom r
12	10	crn 5115	. . . . . 6 class ran r
13	11, 12	cun 3572	. . . . 5 class ( dom r u. ran r )
14	9, 13	cres 5116	. . . 4 class ( _I |` ( dom r u. ran r ) )
15		vx	. . . . . . 7 setvar x
16		vy	. . . . . . 7 setvar y
17	15	cv 1482	. . . . . . . 8 class x
18	17, 10	ccom 5118	. . . . . . 7 class ( x o. r )
19	15, 16, 4, 4, 18	cmpt2 6652	. . . . . 6 class ( x e. _V , y e. _V |-> ( x o. r ) )
20		vz	. . . . . . 7 setvar z
21	20, 4, 10	cmpt 4729	. . . . . 6 class ( z e. _V |-> r )
22		c1 9937	. . . . . 6 class 1
23	19, 21, 22	cseq 12801	. . . . 5 class seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) )
24	6, 23	cfv 5888	. . . 4 class ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n )
25	8, 14, 24	cif 4086	. . 3 class if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) )
26	2, 3, 4, 5, 25	cmpt2 6652	. 2 class ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) )
27	1, 26	wceq 1483	1 wff ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) )

This definition is referenced by:  relexp0g  13762  relexpsucnnr  13765  relexp1g  13766