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 \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crelexp	$class ↑_{r}$
1		vr	$setvar r$
2		cvv	$class V$
3		vn	$setvar n$
4		cn0	$class ℕ_{0}$
5	3	cv	$setvar n$
6		cc0	$class 0$
7	5 6	wceq	$wff n = 0$
8		cid	$class I$
9	1	cv	$setvar r$
10	9	cdm	$class dom r$
11	9	crn	$class ran r$
12	10 11	cun	$class (dom r \cup ran r)$
13	8 12	cres	$class ({I ↾}_{(dom r \cup ran r)})$
14		c1	$class 1$
15		vx	$setvar x$
16		vy	$setvar y$
17	15	cv	$setvar x$
18	17 9	ccom	$class (x \circ r)$
19	15 16 2 2 18	cmpo	$class (x \in V, y \in V ⟼ x \circ r)$
20		vz	$setvar z$
21	20 2 9	cmpt	$class (z \in V ⟼ r)$
22	19 21 14	cseq	$class seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r))$
23	5 22	cfv	$class seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)$
24	7 13 23	cif	$class if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n))$
25	1 3 2 4 24	cmpo	$class (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)))$
26	0 25	wceq	$wff ↑_{r} = (r \in V, n \in ℕ_{0} ⟼ if (n = 0, {I ↾}_{(dom r \cup ran r)}, seq 1 ((x \in V, y \in V ⟼ x \circ r), (z \in V ⟼ r)) (n)))$

Metamath Proof Explorer

Definition df-relexp

Detailed syntax breakdown