Theorem relexp0

Description: A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020)

	Ref	Expression
Assertion	relexp0	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		relexp0g	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
2		relfld	⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )
3	2	reseq2d	⊢ ( Rel 𝑅 → ( I ↾ ∪ ∪ 𝑅 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
4	3	eqcomd	⊢ ( Rel 𝑅 → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( I ↾ ∪ ∪ 𝑅 ) )
5	1 4	sylan9eq	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) )