Metamath Proof Explorer

Theorem relexpreld

Description: The exponentiation of a relation is a relation. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

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

Proof

Step	Hyp	Ref	Expression
1		relexpreld.1	$⊢ φ \to Rel R$
2		relexpreld.2	$⊢ φ \to N \in ℕ_{0}$
3	2	adantr	$⊢ (φ \land R \in V) \to N \in ℕ_{0}$
4		simpr	$⊢ (φ \land R \in V) \to R \in V$
5	1	adantr	$⊢ (φ \land R \in V) \to Rel R$
6		relexprel	$⊢ (N \in ℕ_{0} \land R \in V \land Rel R) \to Rel (R ↑_{r} N)$
7	3 4 5 6	syl3anc	$⊢ (φ \land R \in V) \to Rel (R ↑_{r} N)$
8	7	ex	$⊢ φ \to (R \in V \to Rel (R ↑_{r} N))$
9		rel0	$⊢ Rel \emptyset$
10		reldmrelexp	$⊢ Rel dom ↑_{r}$
11	10	ovprc1	$⊢ \neg R \in V \to R ↑_{r} N = \emptyset$
12	11	releqd	$⊢ \neg R \in V \to (Rel (R ↑_{r} N) \leftrightarrow Rel \emptyset)$
13	9 12	mpbiri	$⊢ \neg R \in V \to Rel (R ↑_{r} N)$
14	8 13	pm2.61d1	$⊢ φ \to Rel (R ↑_{r} N)$