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

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		relexpnnrn	$⊢ (N \in ℕ \land R \in V) \to ran (R ↑_{r} N) \subseteq ran R$
3		ssun2	$⊢ ran R \subseteq dom R \cup ran R$
4	2 3	sstrdi	$⊢ (N \in ℕ \land R \in V) \to ran (R ↑_{r} N) \subseteq dom R \cup ran R$
5	4	ex	$⊢ N \in ℕ \to (R \in V \to ran (R ↑_{r} N) \subseteq dom R \cup ran R)$
6		simpl	$⊢ (N = 0 \land R \in V) \to N = 0$
7	6	oveq2d	$⊢ (N = 0 \land R \in V) \to R ↑_{r} N = R ↑_{r} 0$
8		relexp0g	$⊢ R \in V \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
9	8	adantl	$⊢ (N = 0 \land R \in V) \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
10	7 9	eqtrd	$⊢ (N = 0 \land R \in V) \to R ↑_{r} N = {I ↾}_{(dom R \cup ran R)}$
11	10	rneqd	$⊢ (N = 0 \land R \in V) \to ran (R ↑_{r} N) = ran ({I ↾}_{(dom R \cup ran R)})$
12		rnresi	$⊢ ran ({I ↾}_{(dom R \cup ran R)}) = dom R \cup ran R$
13	11 12	eqtrdi	$⊢ (N = 0 \land R \in V) \to ran (R ↑_{r} N) = dom R \cup ran R$
14		eqimss	$⊢ ran (R ↑_{r} N) = dom R \cup ran R \to ran (R ↑_{r} N) \subseteq dom R \cup ran R$
15	13 14	syl	$⊢ (N = 0 \land R \in V) \to ran (R ↑_{r} N) \subseteq dom R \cup ran R$
16	15	ex	$⊢ N = 0 \to (R \in V \to ran (R ↑_{r} N) \subseteq dom R \cup ran R)$
17	5 16	jaoi	$⊢ (N \in ℕ \lor N = 0) \to (R \in V \to ran (R ↑_{r} N) \subseteq dom R \cup ran R)$
18	1 17	sylbi	$⊢ N \in ℕ_{0} \to (R \in V \to ran (R ↑_{r} N) \subseteq dom R \cup ran R)$
19	18	imp	$⊢ (N \in ℕ_{0} \land R \in V) \to ran (R ↑_{r} N) \subseteq dom R \cup ran R$