Metamath Proof Explorer

Theorem relexpdmg

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 relexpdmg 
|- ( ( N e. NN0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 relexpnndm 
 |-  ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
3 ssun1 
 |-  dom R C_ ( dom R u. ran R )
4 2 3 sstrdi 
 |-  ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
5 4 ex 
 |-  ( N e. NN -> ( R e. V -> dom ( R ^r N ) C_ ( dom R u. ran R ) ) )
6 simpl 
 |-  ( ( N = 0 /\ R e. V ) -> N = 0 )
7 6 oveq2d 
 |-  ( ( N = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
8 relexp0g 
 |-  ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
9 8 adantl 
 |-  ( ( N = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
10 7 9 eqtrd 
 |-  ( ( N = 0 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
11 10 dmeqd 
 |-  ( ( N = 0 /\ R e. V ) -> dom ( R ^r N ) = dom ( _I |` ( dom R u. ran R ) ) )
12 dmresi 
 |-  dom ( _I |` ( dom R u. ran R ) ) = ( dom R u. ran R )
13 11 12 eqtrdi 
 |-  ( ( N = 0 /\ R e. V ) -> dom ( R ^r N ) = ( dom R u. ran R ) )
14 eqimss 
 |-  ( dom ( R ^r N ) = ( dom R u. ran R ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
15 13 14 syl 
 |-  ( ( N = 0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
16 15 ex 
 |-  ( N = 0 -> ( R e. V -> dom ( R ^r N ) C_ ( dom R u. ran R ) ) )
17 5 16 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( R e. V -> dom ( R ^r N ) C_ ( dom R u. ran R ) ) )
18 1 17 sylbi 
 |-  ( N e. NN0 -> ( R e. V -> dom ( R ^r N ) C_ ( dom R u. ran R ) ) )
19 18 imp 
 |-  ( ( N e. NN0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )