Theorem relexpsucld

Description: A reduction for relation exponentiation to the left. (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	relexpsucld	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 ( 𝑁 + 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		relexpsucl	⊢ ( ( 𝑅 ∈ 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	coeq2d	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) = ( 𝑅 ∘ ∅ ) )
13		co02	⊢ ( 𝑅 ∘ ∅ ) = ∅
14	12 13	eqtr2di	⊢ ( ¬ 𝑅 ∈ V → ∅ = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) )
15	10 14	eqtrd	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) )
16	8 15	pm2.61d1	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) )