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	|- ( ph -> Rel R )
	relexpsucrd.2	|- ( ph -> N e. NN0 )
Assertion	relexpsucld	|- ( ph -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )

Proof

Step	Hyp	Ref	Expression
1		relexpsucrd.1	|- ( ph -> Rel R )
2		relexpsucrd.2	|- ( ph -> N e. NN0 )
3		simpr	|- ( ( ph /\ R e. _V ) -> R e. _V )
4	1	adantr	|- ( ( ph /\ R e. _V ) -> Rel R )
5	2	adantr	|- ( ( ph /\ R e. _V ) -> N e. NN0 )
6		relexpsucl	|- ( ( R e. _V /\ Rel R /\ N e. NN0 ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )
7	3 4 5 6	syl3anc	|- ( ( ph /\ R e. _V ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )
8	7	ex	|- ( ph -> ( R e. _V -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) ) )
9		reldmrelexp	|- Rel dom ^r
10	9	ovprc1	|- ( -. R e. _V -> ( R ^r ( N + 1 ) ) = (/) )
11	9	ovprc1	|- ( -. R e. _V -> ( R ^r N ) = (/) )
12	11	coeq2d	|- ( -. R e. _V -> ( R o. ( R ^r N ) ) = ( R o. (/) ) )
13		co02	|- ( R o. (/) ) = (/)
14	12 13	eqtr2di	|- ( -. R e. _V -> (/) = ( R o. ( R ^r N ) ) )
15	10 14	eqtrd	|- ( -. R e. _V -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )
16	8 15	pm2.61d1	|- ( ph -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )