MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-relexp Structured version   Visualization version   Unicode version

Definition df-relexp 13139
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
StepHypRef Expression
1 crelexp 13138 . 2  class ^r
2 vr . . 3  setvar  r
3 vn . . 3  setvar  n
4 cvv 3057 . . 3  class  _V
5 cn0 10903 . . 3  class  NN0
63cv 1454 . . . . 5  class  n
7 cc0 9570 . . . . 5  class  0
86, 7wceq 1455 . . . 4  wff  n  =  0
9 cid 4766 . . . . 5  class  _I
102cv 1454 . . . . . . 7  class  r
1110cdm 4856 . . . . . 6  class  dom  r
1210crn 4857 . . . . . 6  class  ran  r
1311, 12cun 3414 . . . . 5  class  ( dom  r  u.  ran  r
)
149, 13cres 4858 . . . 4  class  (  _I  |`  ( dom  r  u. 
ran  r ) )
15 vx . . . . . . 7  setvar  x
16 vy . . . . . . 7  setvar  y
1715cv 1454 . . . . . . . 8  class  x
1817, 10ccom 4860 . . . . . . 7  class  ( x  o.  r )
1915, 16, 4, 4, 18cmpt2 6322 . . . . . 6  class  ( x  e.  _V ,  y  e.  _V  |->  ( x  o.  r ) )
20 vz . . . . . . 7  setvar  z
2120, 4, 10cmpt 4477 . . . . . 6  class  ( z  e.  _V  |->  r )
22 c1 9571 . . . . . 6  class  1
2319, 21, 22cseq 12251 . . . . 5  class  seq 1
( ( x  e. 
_V ,  y  e. 
_V  |->  ( x  o.  r ) ) ,  ( z  e.  _V  |->  r ) )
246, 23cfv 5605 . . . 4  class  (  seq 1 ( ( x  e.  _V ,  y  e.  _V  |->  ( x  o.  r ) ) ,  ( z  e. 
_V  |->  r ) ) `
 n )
258, 14, 24cif 3893 . . 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
) )
262, 3, 4, 5, 25cmpt2 6322 . 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 ) ) )
271, 26wceq 1455 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 ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  relexp0g  13140  relexpsucnnr  13143  relexp1g  13144
  Copyright terms: Public domain W3C validator