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 e. NN /\ R e. V ) -> ran ( R ^r N ) C_ ran R )

Proof

Step	Hyp	Ref	Expression
1		cnvexg	|- ( R e. V -> `' R e. _V )
2		relexpnndm	|- ( ( N e. NN /\ `' R e. _V ) -> dom ( `' R ^r N ) C_ dom `' R )
3	1 2	sylan2	|- ( ( N e. NN /\ R e. V ) -> dom ( `' R ^r N ) C_ dom `' R )
4		df-rn	|- ran ( R ^r N ) = dom `' ( R ^r N )
5		nnnn0	|- ( N e. NN -> N e. NN0 )
6		relexpcnv	|- ( ( N e. NN0 /\ R e. V ) -> `' ( R ^r N ) = ( `' R ^r N ) )
7	5 6	sylan	|- ( ( N e. NN /\ R e. V ) -> `' ( R ^r N ) = ( `' R ^r N ) )
8	7	dmeqd	|- ( ( N e. NN /\ R e. V ) -> dom `' ( R ^r N ) = dom ( `' R ^r N ) )
9	4 8	eqtrid	|- ( ( N e. NN /\ R e. V ) -> ran ( R ^r N ) = dom ( `' R ^r N ) )
10		df-rn	|- ran R = dom `' R
11	10	a1i	|- ( ( N e. NN /\ R e. V ) -> ran R = dom `' R )
12	3 9 11	3sstr4d	|- ( ( N e. NN /\ R e. V ) -> ran ( R ^r N ) C_ ran R )