Metamath Proof Explorer

Theorem relexpnndm

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 relexpnndm 
|- ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( n = 1 -> ( R ^r n ) = ( R ^r 1 ) )
2 1 dmeqd 
 |-  ( n = 1 -> dom ( R ^r n ) = dom ( R ^r 1 ) )
3 2 sseq1d 
 |-  ( n = 1 -> ( dom ( R ^r n ) C_ dom R <-> dom ( R ^r 1 ) C_ dom R ) )
4 3 imbi2d 
 |-  ( n = 1 -> ( ( R e. V -> dom ( R ^r n ) C_ dom R ) <-> ( R e. V -> dom ( R ^r 1 ) C_ dom R ) ) )
5 oveq2 
 |-  ( n = m -> ( R ^r n ) = ( R ^r m ) )
6 5 dmeqd 
 |-  ( n = m -> dom ( R ^r n ) = dom ( R ^r m ) )
7 6 sseq1d 
 |-  ( n = m -> ( dom ( R ^r n ) C_ dom R <-> dom ( R ^r m ) C_ dom R ) )
8 7 imbi2d 
 |-  ( n = m -> ( ( R e. V -> dom ( R ^r n ) C_ dom R ) <-> ( R e. V -> dom ( R ^r m ) C_ dom R ) ) )
9 oveq2 
 |-  ( n = ( m + 1 ) -> ( R ^r n ) = ( R ^r ( m + 1 ) ) )
10 9 dmeqd 
 |-  ( n = ( m + 1 ) -> dom ( R ^r n ) = dom ( R ^r ( m + 1 ) ) )
11 10 sseq1d 
 |-  ( n = ( m + 1 ) -> ( dom ( R ^r n ) C_ dom R <-> dom ( R ^r ( m + 1 ) ) C_ dom R ) )
12 11 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( R e. V -> dom ( R ^r n ) C_ dom R ) <-> ( R e. V -> dom ( R ^r ( m + 1 ) ) C_ dom R ) ) )
13 oveq2 
 |-  ( n = N -> ( R ^r n ) = ( R ^r N ) )
14 13 dmeqd 
 |-  ( n = N -> dom ( R ^r n ) = dom ( R ^r N ) )
15 14 sseq1d 
 |-  ( n = N -> ( dom ( R ^r n ) C_ dom R <-> dom ( R ^r N ) C_ dom R ) )
16 15 imbi2d 
 |-  ( n = N -> ( ( R e. V -> dom ( R ^r n ) C_ dom R ) <-> ( R e. V -> dom ( R ^r N ) C_ dom R ) ) )
17 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
18 17 dmeqd 
 |-  ( R e. V -> dom ( R ^r 1 ) = dom R )
19 eqimss 
 |-  ( dom ( R ^r 1 ) = dom R -> dom ( R ^r 1 ) C_ dom R )
20 18 19 syl 
 |-  ( R e. V -> dom ( R ^r 1 ) C_ dom R )
21 relexpsucnnr 
 |-  ( ( R e. V /\ m e. NN ) -> ( R ^r ( m + 1 ) ) = ( ( R ^r m ) o. R ) )
22 21 ancoms 
 |-  ( ( m e. NN /\ R e. V ) -> ( R ^r ( m + 1 ) ) = ( ( R ^r m ) o. R ) )
23 22 dmeqd 
 |-  ( ( m e. NN /\ R e. V ) -> dom ( R ^r ( m + 1 ) ) = dom ( ( R ^r m ) o. R ) )
24 dmcoss 
 |-  dom ( ( R ^r m ) o. R ) C_ dom R
25 23 24 eqsstrdi 
 |-  ( ( m e. NN /\ R e. V ) -> dom ( R ^r ( m + 1 ) ) C_ dom R )
26 25 a1d 
 |-  ( ( m e. NN /\ R e. V ) -> ( dom ( R ^r m ) C_ dom R -> dom ( R ^r ( m + 1 ) ) C_ dom R ) )
27 26 ex 
 |-  ( m e. NN -> ( R e. V -> ( dom ( R ^r m ) C_ dom R -> dom ( R ^r ( m + 1 ) ) C_ dom R ) ) )
28 27 a2d 
 |-  ( m e. NN -> ( ( R e. V -> dom ( R ^r m ) C_ dom R ) -> ( R e. V -> dom ( R ^r ( m + 1 ) ) C_ dom R ) ) )
29 4 8 12 16 20 28 nnind 
 |-  ( N e. NN -> ( R e. V -> dom ( R ^r N ) C_ dom R ) )
30 29 imp 
 |-  ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )