Metamath Proof Explorer

Theorem relexpdmg

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

		Ref	Expression
	Assertion	relexpdmg	$⊢ (N \in ℕ_{0} \land R \in V) \to dom (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		relexpnndm	$⊢ (N \in ℕ \land R \in V) \to dom (R ↑_{r} N) \subseteq dom R$
3		ssun1	$⊢ dom R \subseteq dom R \cup ran R$
4	2 3	sstrdi	$⊢ (N \in ℕ \land R \in V) \to dom (R ↑_{r} N) \subseteq dom R \cup ran R$
5	4	ex	$⊢ N \in ℕ \to (R \in V \to dom (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	dmeqd	$⊢ (N = 0 \land R \in V) \to dom (R ↑_{r} N) = dom ({I ↾}_{(dom R \cup ran R)})$
12		dmresi	$⊢ dom ({I ↾}_{(dom R \cup ran R)}) = dom R \cup ran R$
13	11 12	eqtrdi	$⊢ (N = 0 \land R \in V) \to dom (R ↑_{r} N) = dom R \cup ran R$
14		eqimss	$⊢ dom (R ↑_{r} N) = dom R \cup ran R \to dom (R ↑_{r} N) \subseteq dom R \cup ran R$
15	13 14	syl	$⊢ (N = 0 \land R \in V) \to dom (R ↑_{r} N) \subseteq dom R \cup ran R$
16	15	ex	$⊢ N = 0 \to (R \in V \to dom (R ↑_{r} N) \subseteq dom R \cup ran R)$
17	5 16	jaoi	$⊢ (N \in ℕ \lor N = 0) \to (R \in V \to dom (R ↑_{r} N) \subseteq dom R \cup ran R)$
18	1 17	sylbi	$⊢ N \in ℕ_{0} \to (R \in V \to dom (R ↑_{r} N) \subseteq dom R \cup ran R)$
19	18	imp	$⊢ (N \in ℕ_{0} \land R \in V) \to dom (R ↑_{r} N) \subseteq dom R \cup ran R$