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

Proof

Step Hyp Ref Expression
1 elnn0 N 0 N N = 0
2 relexpnndm N R V dom R r N dom R
3 ssun1 dom R dom R ran R
4 2 3 sstrdi N R V dom R r N dom R ran R
5 4 ex N R V dom R r N dom R ran R
6 simpl N = 0 R V N = 0
7 6 oveq2d N = 0 R V R r N = R r 0
8 relexp0g R V R r 0 = I dom R ran R
9 8 adantl N = 0 R V R r 0 = I dom R ran R
10 7 9 eqtrd N = 0 R V R r N = I dom R ran R
11 10 dmeqd N = 0 R V dom R r N = dom I dom R ran R
12 dmresi dom I dom R ran R = dom R ran R
13 11 12 eqtrdi N = 0 R V dom R r N = dom R ran R
14 eqimss dom R r N = dom R ran R dom R r N dom R ran R
15 13 14 syl N = 0 R V dom R r N dom R ran R
16 15 ex N = 0 R V dom R r N dom R ran R
17 5 16 jaoi N N = 0 R V dom R r N dom R ran R
18 1 17 sylbi N 0 R V dom R r N dom R ran R
19 18 imp N 0 R V dom R r N dom R ran R