Metamath Proof Explorer


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

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 relexpsucr
 |-  ( ( R e. _V /\ Rel R /\ N e. NN0 ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )
7 3 4 5 6 syl3anc
 |-  ( ( ph /\ R e. _V ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )
8 7 ex
 |-  ( ph -> ( R e. _V -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) )
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 coeq1d
 |-  ( -. R e. _V -> ( ( R ^r N ) o. R ) = ( (/) o. R ) )
13 co01
 |-  ( (/) o. R ) = (/)
14 12 13 eqtr2di
 |-  ( -. R e. _V -> (/) = ( ( R ^r N ) o. R ) )
15 10 14 eqtrd
 |-  ( -. R e. _V -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )
16 8 15 pm2.61d1
 |-  ( ph -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )