Theorem relexprel

Description: The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020)

	Ref	Expression
Assertion	relexprel	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1	⊢ ( Rel 𝑅 → ( 𝑁 = 1 → Rel 𝑅 ) )
2		relexprelg	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ ( 𝑁 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )
3	1 2	syl3an3	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )