Metamath Proof Explorer


Theorem relexprng

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

Ref Expression
Assertion relexprng N 0 R V ran R r N dom R ran R

Proof

Step Hyp Ref Expression
1 elnn0 N 0 N N = 0
2 relexpnnrn N R V ran R r N ran R
3 ssun2 ran R dom R ran R
4 2 3 sstrdi N R V ran R r N dom R ran R
5 4 ex N R V ran 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 rneqd N = 0 R V ran R r N = ran I dom R ran R
12 rnresi ran I dom R ran R = dom R ran R
13 11 12 eqtrdi N = 0 R V ran R r N = dom R ran R
14 eqimss ran R r N = dom R ran R ran R r N dom R ran R
15 13 14 syl N = 0 R V ran R r N dom R ran R
16 15 ex N = 0 R V ran R r N dom R ran R
17 5 16 jaoi N N = 0 R V ran R r N dom R ran R
18 1 17 sylbi N 0 R V ran R r N dom R ran R
19 18 imp N 0 R V ran R r N dom R ran R