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 \in ℕ \land R \in V) \to ran (R ↑_{r} N) \subseteq ran R$

Step	Hyp	Ref	Expression
1		cnvexg	$⊢ R \in V \to R^{-1} \in V$
2		relexpnndm	$⊢ (N \in ℕ \land R^{-1} \in V) \to dom (R^{-1} ↑_{r} N) \subseteq dom R^{-1}$
3	1 2	sylan2	$⊢ (N \in ℕ \land R \in V) \to dom (R^{-1} ↑_{r} N) \subseteq dom R^{-1}$
4		df-rn	$⊢ ran (R ↑_{r} N) = dom {(R ↑_{r} N)}^{-1}$
5		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
6		relexpcnv	$⊢ (N \in ℕ_{0} \land R \in V) \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N$
7	5 6	sylan	$⊢ (N \in ℕ \land R \in V) \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N$
8	7	dmeqd	$⊢ (N \in ℕ \land R \in V) \to dom {(R ↑_{r} N)}^{-1} = dom (R^{-1} ↑_{r} N)$
9	4 8	eqtrid	$⊢ (N \in ℕ \land R \in V) \to ran (R ↑_{r} N) = dom (R^{-1} ↑_{r} N)$
10		df-rn	$⊢ ran R = dom R^{-1}$
11	10	a1i	$⊢ (N \in ℕ \land R \in V) \to ran R = dom R^{-1}$
12	3 9 11	3sstr4d	$⊢ (N \in ℕ \land R \in V) \to ran (R ↑_{r} N) \subseteq ran R$

Metamath Proof Explorer