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	|- Rel dom ^r

Proof

Step	Hyp	Ref	Expression
1		df-relexp	|- ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) )
2	1	reldmmpo	|- Rel dom ^r