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 𝑟 = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crelexp 𝑟
1 vr 𝑟
2 cvv V
3 vn 𝑛
4 cn0 0
5 3 cv 𝑛
6 cc0 0
7 5 6 wceq 𝑛 = 0
8 cid I
9 1 cv 𝑟
10 9 cdm dom 𝑟
11 9 crn ran 𝑟
12 10 11 cun ( dom 𝑟 ∪ ran 𝑟 )
13 8 12 cres ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) )
14 c1 1
15 vx 𝑥
16 vy 𝑦
17 15 cv 𝑥
18 17 9 ccom ( 𝑥𝑟 )
19 15 16 2 2 18 cmpo ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥𝑟 ) )
20 vz 𝑧
21 20 2 9 cmpt ( 𝑧 ∈ V ↦ 𝑟 )
22 19 21 14 cseq seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) )
23 5 22 cfv ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 )
24 7 13 23 cif if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) )
25 1 3 2 4 24 cmpo ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) )
26 0 25 wceq 𝑟 = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) )