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

Detailed syntax breakdown

Step Hyp Ref Expression
0 crelexp 
 |-  ^r
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vn 
 |-  n
4 cn0 
 |-  NN0
5 3 cv 
 |-  n
6 cc0 
 |-  0
7 5 6 wceq 
 |-  n = 0
8 cid 
 |-  _I
9 1 cv 
 |-  r
10 9 cdm 
 |-  dom r
11 9 crn 
 |-  ran r
12 10 11 cun 
 |-  ( dom r u. ran r )
13 8 12 cres 
 |-  ( _I |` ( dom r u. ran r ) )
14 c1 
 |-  1
15 vx 
 |-  x
16 vy 
 |-  y
17 15 cv 
 |-  x
18 17 9 ccom 
 |-  ( x o. r )
19 15 16 2 2 18 cmpo 
 |-  ( x e. _V , y e. _V |-> ( x o. r ) )
20 vz 
 |-  z
21 20 2 9 cmpt 
 |-  ( z e. _V |-> r )
22 19 21 14 cseq 
 |-  seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) )
23 5 22 cfv 
 |-  ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n )
24 7 13 23 cif 
 |-  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 ) )
25 1 3 2 4 24 cmpo 
 |-  ( 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 ) ) )
26 0 25 wceq 
 |-  ^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 ) ) )