Theorem reldmrelexp

Description: The domain of the repeated composition of a relation is a relation. (Contributed by AV, 12-Jul-2024)

	Ref	Expression
Assertion	reldmrelexp	$$⊢\mathrm{Rel}\mathrm{dom}{\uparrow }_r$$

Proof

Step	Hyp	Ref	Expression
1		df-relexp	$$⊢{\uparrow }_r=\left(r\in \mathrm{V},n\in {\mathbb{N}}_0⟼if\left(n=0,{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}r\cup \mathrm{ran}r\right)},seq1\left(\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\circ r\right),\left(z\in \mathrm{V}⟼r\right)\right)\left(n\right)\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}{\uparrow }_r$$