Metamath Proof Explorer

Theorem relexpdm

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

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

Proof

Step Hyp Ref Expression
1 relexpdmg 
 |-  ( ( N e. NN0 /\ R e. V ) -> dom ( 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 ) -> dom ( R ^r N ) C_ U. U. R )