Users' Mathboxes Mathbox for Drahflow < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-relexp Structured version   Unicode version

Definition df-relexp 27329
Description: Definition of repeated composition of a relation with itself, aka relation exponentiation. (Contributed by Drahflow, 12-Nov-2015.)
Assertion
Ref Expression
df-relexp  |-  ^r  =  ( r  e. 
_V ,  n  e. 
NN0  |->  (  seq 0
( ( x  e. 
_V ,  y  e. 
_V  |->  ( x  o.  r ) ) ,  ( z  e.  _V  |->  (  _I  |`  U. U. r ) ) ) `
 n ) )
Distinct variable group:    n, r, x, y, z

Detailed syntax breakdown of Definition df-relexp
StepHypRef Expression
1 crelexp 27328 . 2  class  ^r
2 vr . . 3  setvar  r
3 vn . . 3  setvar  n
4 cvv 2971 . . 3  class  _V
5 cn0 10578 . . 3  class  NN0
63cv 1368 . . . 4  class  n
7 vx . . . . . 6  setvar  x
8 vy . . . . . 6  setvar  y
97cv 1368 . . . . . . 7  class  x
102cv 1368 . . . . . . 7  class  r
119, 10ccom 4843 . . . . . 6  class  ( x  o.  r )
127, 8, 4, 4, 11cmpt2 6092 . . . . 5  class  ( x  e.  _V ,  y  e.  _V  |->  ( x  o.  r ) )
13 vz . . . . . 6  setvar  z
14 cid 4630 . . . . . . 7  class  _I
1510cuni 4090 . . . . . . . 8  class  U. r
1615cuni 4090 . . . . . . 7  class  U. U. r
1714, 16cres 4841 . . . . . 6  class  (  _I  |`  U. U. r )
1813, 4, 17cmpt 4349 . . . . 5  class  ( z  e.  _V  |->  (  _I  |`  U. U. r ) )
19 cc0 9281 . . . . 5  class  0
2012, 18, 19cseq 11805 . . . 4  class  seq 0
( ( x  e. 
_V ,  y  e. 
_V  |->  ( x  o.  r ) ) ,  ( z  e.  _V  |->  (  _I  |`  U. U. r ) ) )
216, 20cfv 5417 . . 3  class  (  seq 0 ( ( x  e.  _V ,  y  e.  _V  |->  ( x  o.  r ) ) ,  ( z  e. 
_V  |->  (  _I  |`  U. U. r ) ) ) `
 n )
222, 3, 4, 5, 21cmpt2 6092 . 2  class  ( r  e.  _V ,  n  e.  NN0  |->  (  seq 0
( ( x  e. 
_V ,  y  e. 
_V  |->  ( x  o.  r ) ) ,  ( z  e.  _V  |->  (  _I  |`  U. U. r ) ) ) `
 n ) )
231, 22wceq 1369 1  wff  ^r  =  ( r  e. 
_V ,  n  e. 
NN0  |->  (  seq 0
( ( x  e. 
_V ,  y  e. 
_V  |->  ( x  o.  r ) ) ,  ( z  e.  _V  |->  (  _I  |`  U. U. r ) ) ) `
 n ) )
Colors of variables: wff setvar class
This definition is referenced by:  relexp0  27330  relexpsucr  27331
  Copyright terms: Public domain W3C validator