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

Definition df-relexp 13742
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 𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))
Distinct variable group:   𝑛,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-relexp
StepHypRef Expression
1 crelexp 13741 . 2 class 𝑟
2 vr . . 3 setvar 𝑟
3 vn . . 3 setvar 𝑛
4 cvv 3195 . . 3 class V
5 cn0 11277 . . 3 class 0
63cv 1480 . . . . 5 class 𝑛
7 cc0 9921 . . . . 5 class 0
86, 7wceq 1481 . . . 4 wff 𝑛 = 0
9 cid 5013 . . . . 5 class I
102cv 1480 . . . . . . 7 class 𝑟
1110cdm 5104 . . . . . 6 class dom 𝑟
1210crn 5105 . . . . . 6 class ran 𝑟
1311, 12cun 3565 . . . . 5 class (dom 𝑟 ∪ ran 𝑟)
149, 13cres 5106 . . . 4 class ( I ↾ (dom 𝑟 ∪ ran 𝑟))
15 vx . . . . . . 7 setvar 𝑥
16 vy . . . . . . 7 setvar 𝑦
1715cv 1480 . . . . . . . 8 class 𝑥
1817, 10ccom 5108 . . . . . . 7 class (𝑥𝑟)
1915, 16, 4, 4, 18cmpt2 6637 . . . . . 6 class (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟))
20 vz . . . . . . 7 setvar 𝑧
2120, 4, 10cmpt 4720 . . . . . 6 class (𝑧 ∈ V ↦ 𝑟)
22 c1 9922 . . . . . 6 class 1
2319, 21, 22cseq 12784 . . . . 5 class seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))
246, 23cfv 5876 . . . 4 class (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)
258, 14, 24cif 4077 . . 3 class if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛))
262, 3, 4, 5, 25cmpt2 6637 . 2 class (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))
271, 26wceq 1481 1 wff 𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))
Colors of variables: wff setvar class
This definition is referenced by:  relexp0g  13743  relexpsucnnr  13746  relexp1g  13747
  Copyright terms: Public domain W3C validator