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 ↑𝑟

Proof

Step	Hyp	Ref	Expression
1		df-relexp	⊢ ↑𝑟 = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) )
2	1	reldmmpo	⊢ Rel dom ↑𝑟