Metamath Proof Explorer


Theorem relexpnnrn

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

Proof

Step Hyp Ref Expression
1 cnvexg R V R -1 V
2 relexpnndm N R -1 V dom R -1 r N dom R -1
3 1 2 sylan2 N R V dom R -1 r N dom R -1
4 df-rn ran R r N = dom R r N -1
5 nnnn0 N N 0
6 relexpcnv N 0 R V R r N -1 = R -1 r N
7 5 6 sylan N R V R r N -1 = R -1 r N
8 7 dmeqd N R V dom R r N -1 = dom R -1 r N
9 4 8 syl5eq N R V ran R r N = dom R -1 r N
10 df-rn ran R = dom R -1
11 10 a1i N R V ran R = dom R -1
12 3 9 11 3sstr4d N R V ran R r N ran R