Theorem relexp0d

Description: A relation composed zero times is the (restricted) identity. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypotheses	relexp0d.1	⊢ ( 𝜑 → Rel 𝑅 )
	relexp0d.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
Assertion	relexp0d	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		relexp0d.1	⊢ ( 𝜑 → Rel 𝑅 )
2		relexp0d.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
3		relexp0	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) )
4	2 1 3	syl2anc	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) )