Metamath Proof Explorer

Theorem relexpsucrd

Description: A reduction for relation exponentiation to the right. (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	relexpsucrd	$⊢ φ \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$

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		relexpsucr	$⊢ (R \in V \land Rel R \land N \in ℕ_{0}) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$
7	3 4 5 6	syl3anc	$⊢ (φ \land R \in V) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$
8	7	ex	$⊢ φ \to (R \in V \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R)$
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	coeq1d	$⊢ \neg R \in V \to (R ↑_{r} N) \circ R = \emptyset \circ R$
13		co01	$⊢ \emptyset \circ R = \emptyset$
14	12 13	eqtr2di	$⊢ \neg R \in V \to \emptyset = (R ↑_{r} N) \circ R$
15	10 14	eqtrd	$⊢ \neg R \in V \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$
16	8 15	pm2.61d1	$⊢ φ \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$