Metamath Proof Explorer

Theorem relexpsucld

Description: A reduction for relation exponentiation to the left. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

		Ref	Expression
	Hypotheses	relexpsucrd.1	$⊢ φ \to Rel R$
		relexpsucrd.2	$⊢ φ \to N \in ℕ_{0}$
	Assertion	relexpsucld	$⊢ φ \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)$

Proof

Step	Hyp	Ref	Expression
1		relexpsucrd.1	$⊢ φ \to Rel R$
2		relexpsucrd.2	$⊢ φ \to N \in ℕ_{0}$
3		simpr	$⊢ (φ \land R \in V) \to R \in V$
4	1	adantr	$⊢ (φ \land R \in V) \to Rel R$
5	2	adantr	$⊢ (φ \land R \in V) \to N \in ℕ_{0}$
6		relexpsucl	$⊢ (R \in V \land Rel R \land N \in ℕ_{0}) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)$
7	3 4 5 6	syl3anc	$⊢ (φ \land R \in V) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)$
8	7	ex	$⊢ φ \to (R \in V \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N))$
9		reldmrelexp	$⊢ Rel dom ↑_{r}$
10	9	ovprc1	$⊢ \neg R \in V \to R ↑_{r} (N + 1) = \emptyset$
11	9	ovprc1	$⊢ \neg R \in V \to R ↑_{r} N = \emptyset$
12	11	coeq2d	$⊢ \neg R \in V \to R \circ (R ↑_{r} N) = R \circ \emptyset$
13		co02	$⊢ R \circ \emptyset = \emptyset$
14	12 13	eqtr2di	$⊢ \neg R \in V \to \emptyset = R \circ (R ↑_{r} N)$
15	10 14	eqtrd	$⊢ \neg R \in V \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)$
16	8 15	pm2.61d1	$⊢ φ \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)$