Theorem relexpsucrd

Description: A reduction for relation exponentiation to the right. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypotheses	relexpsucrd.1	⊢ ( 𝜑 → Rel 𝑅 )
	relexpsucrd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	relexpsucrd	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑁 ) ∘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		relexpsucrd.1	⊢ ( 𝜑 → Rel 𝑅 )
2		relexpsucrd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3		simpr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑅 ∈ V )
4	1	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → Rel 𝑅 )
5	2	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑁 ∈ ℕ0 )
6		relexpsucr	⊢ ( ( 𝑅 ∈ V ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑁 ) ∘ 𝑅 ) )
7	3 4 5 6	syl3anc	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑁 ) ∘ 𝑅 ) )
8	7	ex	⊢ ( 𝜑 → ( 𝑅 ∈ V → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑁 ) ∘ 𝑅 ) ) )
9		reldmrelexp	⊢ Rel dom ↑𝑟
10	9	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ∅ )
11	9	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 𝑁 ) = ∅ )
12	11	coeq1d	⊢ ( ¬ 𝑅 ∈ V → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ 𝑅 ) = ( ∅ ∘ 𝑅 ) )
13		co01	⊢ ( ∅ ∘ 𝑅 ) = ∅
14	12 13	eqtr2di	⊢ ( ¬ 𝑅 ∈ V → ∅ = ( ( 𝑅 ↑𝑟 𝑁 ) ∘ 𝑅 ) )
15	10 14	eqtrd	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑁 ) ∘ 𝑅 ) )
16	8 15	pm2.61d1	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑁 ) ∘ 𝑅 ) )