Metamath Proof Explorer

Theorem relexpfld

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

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N = 1 /\ ( N e. NN0 /\ R e. V ) ) -> N = 1 )
2 1 oveq2d 
 |-  ( ( N = 1 /\ ( N e. NN0 /\ R e. V ) ) -> ( R ^r N ) = ( R ^r 1 ) )
3 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
4 3 ad2antll 
 |-  ( ( N = 1 /\ ( N e. NN0 /\ R e. V ) ) -> ( R ^r 1 ) = R )
5 2 4 eqtrd 
 |-  ( ( N = 1 /\ ( N e. NN0 /\ R e. V ) ) -> ( R ^r N ) = R )
6 5 unieqd 
 |-  ( ( N = 1 /\ ( N e. NN0 /\ R e. V ) ) -> U. ( R ^r N ) = U. R )
7 6 unieqd 
 |-  ( ( N = 1 /\ ( N e. NN0 /\ R e. V ) ) -> U. U. ( R ^r N ) = U. U. R )
8 eqimss 
 |-  ( U. U. ( R ^r N ) = U. U. R -> U. U. ( R ^r N ) C_ U. U. R )
9 7 8 syl 
 |-  ( ( N = 1 /\ ( N e. NN0 /\ R e. V ) ) -> U. U. ( R ^r N ) C_ U. U. R )
10 9 ex 
 |-  ( N = 1 -> ( ( N e. NN0 /\ R e. V ) -> U. U. ( R ^r N ) C_ U. U. R ) )
11 simp2 
 |-  ( ( -. N = 1 /\ N e. NN0 /\ R e. V ) -> N e. NN0 )
12 simp3 
 |-  ( ( -. N = 1 /\ N e. NN0 /\ R e. V ) -> R e. V )
13 simp1 
 |-  ( ( -. N = 1 /\ N e. NN0 /\ R e. V ) -> -. N = 1 )
14 13 pm2.21d 
 |-  ( ( -. N = 1 /\ N e. NN0 /\ R e. V ) -> ( N = 1 -> Rel R ) )
15 11 12 14 3jca 
 |-  ( ( -. N = 1 /\ N e. NN0 /\ R e. V ) -> ( N e. NN0 /\ R e. V /\ ( N = 1 -> Rel R ) ) )
16 relexprelg 
 |-  ( ( N e. NN0 /\ R e. V /\ ( N = 1 -> Rel R ) ) -> Rel ( R ^r N ) )
17 relfld 
 |-  ( Rel ( R ^r N ) -> U. U. ( R ^r N ) = ( dom ( R ^r N ) u. ran ( R ^r N ) ) )
18 15 16 17 3syl 
 |-  ( ( -. N = 1 /\ N e. NN0 /\ R e. V ) -> U. U. ( R ^r N ) = ( dom ( R ^r N ) u. ran ( R ^r N ) ) )
19 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
20 relexpnndm 
 |-  ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
21 relexpnnrn 
 |-  ( ( N e. NN /\ R e. V ) -> ran ( R ^r N ) C_ ran R )
22 unss12 
 |-  ( ( dom ( R ^r N ) C_ dom R /\ ran ( R ^r N ) C_ ran R ) -> ( dom ( R ^r N ) u. ran ( R ^r N ) ) C_ ( dom R u. ran R ) )
23 20 21 22 syl2anc 
 |-  ( ( N e. NN /\ R e. V ) -> ( dom ( R ^r N ) u. ran ( R ^r N ) ) C_ ( dom R u. ran R ) )
24 23 ex 
 |-  ( N e. NN -> ( R e. V -> ( dom ( R ^r N ) u. ran ( R ^r N ) ) C_ ( dom R u. ran R ) ) )
25 simpl 
 |-  ( ( N = 0 /\ R e. V ) -> N = 0 )
26 25 oveq2d 
 |-  ( ( N = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
27 relexp0g 
 |-  ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
28 27 adantl 
 |-  ( ( N = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
29 26 28 eqtrd 
 |-  ( ( N = 0 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
30 29 dmeqd 
 |-  ( ( N = 0 /\ R e. V ) -> dom ( R ^r N ) = dom ( _I |` ( dom R u. ran R ) ) )
31 dmresi 
 |-  dom ( _I |` ( dom R u. ran R ) ) = ( dom R u. ran R )
32 30 31 eqtrdi 
 |-  ( ( N = 0 /\ R e. V ) -> dom ( R ^r N ) = ( dom R u. ran R ) )
33 eqimss 
 |-  ( dom ( R ^r N ) = ( dom R u. ran R ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
34 32 33 syl 
 |-  ( ( N = 0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
35 29 rneqd 
 |-  ( ( N = 0 /\ R e. V ) -> ran ( R ^r N ) = ran ( _I |` ( dom R u. ran R ) ) )
36 rnresi 
 |-  ran ( _I |` ( dom R u. ran R ) ) = ( dom R u. ran R )
37 35 36 eqtrdi 
 |-  ( ( N = 0 /\ R e. V ) -> ran ( R ^r N ) = ( dom R u. ran R ) )
38 eqimss 
 |-  ( ran ( R ^r N ) = ( dom R u. ran R ) -> ran ( R ^r N ) C_ ( dom R u. ran R ) )
39 37 38 syl 
 |-  ( ( N = 0 /\ R e. V ) -> ran ( R ^r N ) C_ ( dom R u. ran R ) )
40 34 39 unssd 
 |-  ( ( N = 0 /\ R e. V ) -> ( dom ( R ^r N ) u. ran ( R ^r N ) ) C_ ( dom R u. ran R ) )
41 40 ex 
 |-  ( N = 0 -> ( R e. V -> ( dom ( R ^r N ) u. ran ( R ^r N ) ) C_ ( dom R u. ran R ) ) )
42 24 41 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( R e. V -> ( dom ( R ^r N ) u. ran ( R ^r N ) ) C_ ( dom R u. ran R ) ) )
43 19 42 sylbi 
 |-  ( N e. NN0 -> ( R e. V -> ( dom ( R ^r N ) u. ran ( R ^r N ) ) C_ ( dom R u. ran R ) ) )
44 11 12 43 sylc 
 |-  ( ( -. N = 1 /\ N e. NN0 /\ R e. V ) -> ( dom ( R ^r N ) u. ran ( R ^r N ) ) C_ ( dom R u. ran R ) )
45 18 44 eqsstrd 
 |-  ( ( -. N = 1 /\ N e. NN0 /\ R e. V ) -> U. U. ( R ^r N ) C_ ( dom R u. ran R ) )
46 dmrnssfld 
 |-  ( dom R u. ran R ) C_ U. U. R
47 45 46 sstrdi 
 |-  ( ( -. N = 1 /\ N e. NN0 /\ R e. V ) -> U. U. ( R ^r N ) C_ U. U. R )
48 47 3expib 
 |-  ( -. N = 1 -> ( ( N e. NN0 /\ R e. V ) -> U. U. ( R ^r N ) C_ U. U. R ) )
49 10 48 pm2.61i 
 |-  ( ( N e. NN0 /\ R e. V ) -> U. U. ( R ^r N ) C_ U. U. R )