Metamath Proof Explorer

Theorem relexprel

Description: The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020)

Ref Expression
Assertion relexprel 
|- ( ( N e. NN0 /\ R e. V /\ Rel R ) -> Rel ( R ^r N ) )

Proof

Step Hyp Ref Expression
1 ax-1 
 |-  ( Rel R -> ( N = 1 -> Rel R ) )
2 relexprelg 
 |-  ( ( N e. NN0 /\ R e. V /\ ( N = 1 -> Rel R ) ) -> Rel ( R ^r N ) )
3 1 2 syl3an3 
 |-  ( ( N e. NN0 /\ R e. V /\ Rel R ) -> Rel ( R ^r N ) )