Metamath Proof Explorer

Theorem relexprn

Description: The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020)

Ref Expression
Assertion relexprn 
|- ( ( N e. NN0 /\ R e. V ) -> ran ( R ^r N ) C_ U. U. R )

Proof

Step Hyp Ref Expression
1 relexprng 
 |-  ( ( N e. NN0 /\ R e. V ) -> ran ( R ^r N ) C_ ( dom R u. ran R ) )
2 dmrnssfld 
 |-  ( dom R u. ran R ) C_ U. U. R
3 1 2 sstrdi 
 |-  ( ( N e. NN0 /\ R e. V ) -> ran ( R ^r N ) C_ U. U. R )