Theorem relexp2

Description: A set operated on by the relation exponent to the second power is equal to the composition of the set with itself. (Contributed by RP, 1-Jun-2020)

	Ref	Expression
Assertion	relexp2	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 2 ) = ( 𝑅 ∘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		df-2	⊢ 2 = ( 1 + 1 )
2	1	oveq2i	⊢ ( 𝑅 ↑𝑟 2 ) = ( 𝑅 ↑𝑟 ( 1 + 1 ) )
3	2	a1i	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 2 ) = ( 𝑅 ↑𝑟 ( 1 + 1 ) ) )
4		1nn	⊢ 1 ∈ ℕ
5		relexpsucnnr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 1 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 1 + 1 ) ) = ( ( 𝑅 ↑𝑟 1 ) ∘ 𝑅 ) )
6	4 5	mpan2	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 1 + 1 ) ) = ( ( 𝑅 ↑𝑟 1 ) ∘ 𝑅 ) )
7		relexp1g	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
8	7	coeq1d	⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 1 ) ∘ 𝑅 ) = ( 𝑅 ∘ 𝑅 ) )
9	3 6 8	3eqtrd	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 2 ) = ( 𝑅 ∘ 𝑅 ) )