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 0 R V R r N R

Proof

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