relexpnndm

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ n = 1 \to R ↑_{r} n = R ↑_{r} 1$
2	1	dmeqd	$⊢ n = 1 \to dom (R ↑_{r} n) = dom (R ↑_{r} 1)$
3	2	sseq1d	$⊢ n = 1 \to (dom (R ↑_{r} n) \subseteq dom R \leftrightarrow dom (R ↑_{r} 1) \subseteq dom R)$
4	3	imbi2d	$⊢ n = 1 \to ((R \in V \to dom (R ↑_{r} n) \subseteq dom R) \leftrightarrow (R \in V \to dom (R ↑_{r} 1) \subseteq dom R))$
5		oveq2	$⊢ n = m \to R ↑_{r} n = R ↑_{r} m$
6	5	dmeqd	$⊢ n = m \to dom (R ↑_{r} n) = dom (R ↑_{r} m)$
7	6	sseq1d	$⊢ n = m \to (dom (R ↑_{r} n) \subseteq dom R \leftrightarrow dom (R ↑_{r} m) \subseteq dom R)$
8	7	imbi2d	$⊢ n = m \to ((R \in V \to dom (R ↑_{r} n) \subseteq dom R) \leftrightarrow (R \in V \to dom (R ↑_{r} m) \subseteq dom R))$
9		oveq2	$⊢ n = m + 1 \to R ↑_{r} n = R ↑_{r} (m + 1)$
10	9	dmeqd	$⊢ n = m + 1 \to dom (R ↑_{r} n) = dom (R ↑_{r} (m + 1))$
11	10	sseq1d	$⊢ n = m + 1 \to (dom (R ↑_{r} n) \subseteq dom R \leftrightarrow dom (R ↑_{r} (m + 1)) \subseteq dom R)$
12	11	imbi2d	$⊢ n = m + 1 \to ((R \in V \to dom (R ↑_{r} n) \subseteq dom R) \leftrightarrow (R \in V \to dom (R ↑_{r} (m + 1)) \subseteq dom R))$
13		oveq2	$⊢ n = N \to R ↑_{r} n = R ↑_{r} N$
14	13	dmeqd	$⊢ n = N \to dom (R ↑_{r} n) = dom (R ↑_{r} N)$
15	14	sseq1d	$⊢ n = N \to (dom (R ↑_{r} n) \subseteq dom R \leftrightarrow dom (R ↑_{r} N) \subseteq dom R)$
16	15	imbi2d	$⊢ n = N \to ((R \in V \to dom (R ↑_{r} n) \subseteq dom R) \leftrightarrow (R \in V \to dom (R ↑_{r} N) \subseteq dom R))$
17		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
18	17	dmeqd	$⊢ R \in V \to dom (R ↑_{r} 1) = dom R$
19		eqimss	$⊢ dom (R ↑_{r} 1) = dom R \to dom (R ↑_{r} 1) \subseteq dom R$
20	18 19	syl	$⊢ R \in V \to dom (R ↑_{r} 1) \subseteq dom R$
21		relexpsucnnr	$⊢ (R \in V \land m \in ℕ) \to R ↑_{r} (m + 1) = (R ↑_{r} m) \circ R$
22	21	ancoms	$⊢ (m \in ℕ \land R \in V) \to R ↑_{r} (m + 1) = (R ↑_{r} m) \circ R$
23	22	dmeqd	$⊢ (m \in ℕ \land R \in V) \to dom (R ↑_{r} (m + 1)) = dom ((R ↑_{r} m) \circ R)$
24		dmcoss	$⊢ dom ((R ↑_{r} m) \circ R) \subseteq dom R$
25	23 24	eqsstrdi	$⊢ (m \in ℕ \land R \in V) \to dom (R ↑_{r} (m + 1)) \subseteq dom R$
26	25	a1d	$⊢ (m \in ℕ \land R \in V) \to (dom (R ↑_{r} m) \subseteq dom R \to dom (R ↑_{r} (m + 1)) \subseteq dom R)$
27	26	ex	$⊢ m \in ℕ \to (R \in V \to (dom (R ↑_{r} m) \subseteq dom R \to dom (R ↑_{r} (m + 1)) \subseteq dom R))$
28	27	a2d	$⊢ m \in ℕ \to ((R \in V \to dom (R ↑_{r} m) \subseteq dom R) \to (R \in V \to dom (R ↑_{r} (m + 1)) \subseteq dom R))$
29	4 8 12 16 20 28	nnind	$⊢ N \in ℕ \to (R \in V \to dom (R ↑_{r} N) \subseteq dom R)$
30	29	imp	$⊢ (N \in ℕ \land R \in V) \to dom (R ↑_{r} N) \subseteq dom R$

Metamath Proof Explorer

Theorem relexpnndm

Proof